alt Hacker NewsWhat does it mean for verification to be efficient?
Are there benchmarks showing dafny is faster than other inefficient options ?
What does it mean for verification to be efficient?
Are there benchmarks showing dafny is faster than other inefficient options ?
Dafny 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.