3 ms·

That's exactly what Ada2012 and SPARK2014 did. You write your contracts (preconditions, postconditions, assertions, contract-cases, invariants, type predicates)

That's exactly what Ada2012 and SPARK2014 did. You write your contracts (preconditions, postconditions, assertions, contract-cases, invariants, type predicates) in Ada syntax and you get both runtime assertions and proof depending on which tool you call (compiler or prover). You give more facts when proof fails. You can tag code as 'ghost' and it's only available for proof tools... To be able to be a bit more 'terse' in assertions, they added quantifiers, expression functions, case- and if-expressions. Lots of small improvements to allow contracts, that are finally a boon to write simpler and clearer code. Everything you're asking for here is available in Ada2012 and SPARK2014.

nextaccountic 5y ago
also what https://github.com/facebookexperimental/MIRAI https://github.com/facebookexperimental/MIRAI does for rust: you add contracts (preconditions, postconditions, and invariants) using https://docs.rs/contracts/0.6.0/contracts/ https://docs.rs/contracts/0.6.0/contracts/ and it checks whether they are true here is an example using mirai and contracts: https://github.com/facebookexperimental/MIRAI/blob/master/examples/shopping_cart/src/main.rs https://github.com/facebookexperimental/MIRAI/blob/master/ex... (note: the contracts crate can be used for verifying at runtime as well)
- touisteur 5y ago
  Ah yes, the power of rust's macros. I think there is danger in proposing 'assume' without at least trying to prove it and say you're wrong. I think in spark 'assume' is a guide, but it is checked and it is great, because footguns.