@puffnfresh I have a ponies and unicorns dream for something I think dependent types can do. Care to indulge me?
-
-
Replying to @puffnfresh
@puffnfresh proving certain values are branch-independent (for cache timing-resistant cryptography)2 replies 0 retweets 0 likes -
Replying to @puffnfresh
@puffnfresh a language that proves that no branch depends on a secret value1 reply 0 retweets 1 like -
Replying to @bascule
@bascule Sounds more like a job for modal types or substructural types than dependent types. /cc@puffnfresh1 reply 0 retweets 0 likes -
Replying to @awelonblue
@bascule Modal types would model secret values as existing on a machine that lacks branching, but provides cryptographic prims.@puffnfresh1 reply 0 retweets 0 likes
Replying to @awelonblue
@awelonblue @puffnfresh what I'd actually like to do is prove things about the safe part of Rust programs
10:49 PM - 2 Oct 2014
0 replies
0 retweets
0 likes
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.