4 ms·
The semantics of Dafny is carefully designed to make verification efficient. Dafny can compile to and interface with a few languages, including C#.
by nextos 10mo ago
The semantics of Dafny is carefully designed to make verification efficient.
Dafny can compile to and interface with a few languages, including C#.
- fooker 10mo agoWhat does it mean for verification to be efficient? Are there benchmarks showing dafny is faster than other inefficient options ?
- hatefulmoron 10mo agoDafny and similar languages use SMT; their semantics need to be such that you're giving enough information for your proof to verify in sufficient time, otherwise you'll be waiting for a very long time or your proof is basically undecidable. I'm not sure about benchmarks comparing languages, but Dafny goes through a lot of tweaking to make the process faster.