3 ms·
"Dafny’s ability to statically check critical properties of your program goes well beyond what mainstream languages can do (that includes you, Rust)." Ada supp
by thesuperbigfrog 3y ago
"Dafny’s ability to statically check critical properties of your program goes well beyond what mainstream languages can do (that includes you, Rust)."
Ada supports Design by Contract preconditions, postconditions, and type invariants that were pioneered by the Eiffel programming language:
https://learn.adacore.com/courses/intro-to-ada/chapters/contracts.html https://learn.adacore.com/courses/intro-to-ada/chapters/cont...
The SPARK subset of Ada also does static proofs / formal verification:
https://learn.adacore.com/courses/intro-to-spark/chapters/01_Overview.html https://learn.adacore.com/courses/intro-to-spark/chapters/01...
===
Rust has Design by Contract capabilities via the contracts crate:
https://docs.rs/contracts/latest/contracts/ https://docs.rs/contracts/latest/contracts/
Maybe one day Rust will have formal verification too?
Work is under way: https://alastairreid.github.io/automatic-rust-verification-tools-2021/ https://alastairreid.github.io/automatic-rust-verification-t...
- lionkor 3y ago> Rust has Design by Contract capabilities via the contracts crate And C++ has reflection using boost ;)
- thesuperbigfrog 3y agoContracts for C++ have been proposed: https://www.reddit.com/r/cpp/comments/cmk7ek/what_happened_to_c20_contracts/ https://www.reddit.com/r/cpp/comments/cmk7ek/what_happened_t... Not sure if / when they will land: https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2022/p0592r5.html https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2022/p05...
- jakuj 3y agoYou might be interested in the Prusti project, which statically checks for absence of reachable panics, overflows etc. It also allows user-defined specifications such as pre and post-conditions, loop body invariants, termination checking and so on. https://github.com/viperproject/prusti-dev https://github.com/viperproject/prusti-dev
- perlgeek 3y agoIn Eiffel at least, the contracts are checked at run time, whereas in Dafny it seems that it's verified at compile time. I think (but I'm not sure) that Eiffel disables recursive contract checking (so checking a contract of a function used for checking the contract), so you could put the check for the inverse in each of the function's post conditions, but it would be quite the performance hit to verify it at each call.
- redjamjar 3y agoYeah, SPARK/Ada is a comparable system to Dafny. I agree with that! Also, Frama-C and a bunch of other more esoteric research languages as well.