[gz09]

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]

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.

[esafak]

This expressiveness is a curious point, because a common charge leveled against Scala is that it is too expressive.

[steego]

Expressiveness 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.