5 ms·
It'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 pr
by gz09 9mo ago
It'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).
- ted_dunning 9mo agoInterestingly, 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.
- esafak 9mo agoThis expressiveness is a curious point, because a common charge leveled against Scala is that it is too expressive.
- steego 9mo agoExpressiveness tends to become a liability when the benefits of the expressiveness aren’t clear. Dafny’s expressiveness tends to be more in the service of coherent specifications and less in the service of language abstraction for its own sake.