|
|
|
|
|
|
by hatefulmoron
186 days ago
|
|
|
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. |
|
|