3 ms·
I'm totally unfamiliar with Dafny, the front page didn't do much more than specicify the goals. Any chance you could briefly compare it to Rust or another syst
by bluejekyll 10y ago
I'm totally unfamiliar with Dafny, the front page didn't do much more than specicify the goals.
Any chance you could briefly compare it to Rust or another systems level language trying to remove undefined behavior?
- nickpsecurity 10y agoIt's more like SPARK Ada. It's a limited language designed for easy analysis by an automated prover. You can do preconditions, postconditions, and invariants in it. It was used in ExpressOS for mobile and I think IronClad Apps, too.
- bluejekyll 10y agoAre those pre and post conditions always executed? Or are they optional assertions that can be enabled/disabled?
- neilparikh 10y agoIf I'm reading the description correctly, the pre and post conditions are analyzed statically during compiling, and not added to the output code. So it's a similar idea to type checking, where the program won't even compile until the versifier is sure your code meets the conditions.