@puffnfresh I have a ponies and unicorns dream for something I think dependent types can do. Care to indulge me?
@puffnfresh proving certain values are branch-independent (for cache timing-resistant cryptography)
-
-
@bascule oh, a language which proves branches are timed the same? -
@puffnfresh a language that proves that no branch depends on a secret value -
@bascule Sounds more like a job for modal types or substructural types than dependent types. /cc@puffnfresh -
@bascule Modal types would model secret values as existing on a machine that lacks branching, but provides cryptographic prims.@puffnfresh -
@awelonblue@puffnfresh what I'd actually like to do is prove things about the safe part of Rust programs
End of conversation
New conversation -
-
-
@bascule does that mean a sub-language without branches? Could that just be a DSL?Thanks. Twitter will use this to make your timeline better. UndoUndo
-
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.