alt Hacker NewsIt's similar in spirit, but in Dafny one can express much more complicated and complex invariants which get checked at build time -- compared to eiffel where pre/post conditions are checked at runtime (in dev builds mostly).
Replies
esafak • yesterday at 4:37 AM
This expressiveness is a curious point, because a common charge leveled against Scala is that it is too expressive.
➕ show 1 reply
Interestingly, though, you can have some runtime checking with Dafny as well as the formidable dependent type checking and formal verification that happens at build time.
That means that most of the proof can be done ahead of time with just some loose ends verified using an SMT prover at runtime.