Kind: A Modern Proof Language

Re:Kind: A Modern Proof Language by touisteur on Wednesday August 11, 2021 @04:04PM (#28147025)

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.

[ Parent | on HN ]

Re:Kind: A Modern Proof Language by nextaccountic on Wednesday August 11, 2021 @04:26PM (#28147301)

also what https://github.com/facebookexperimental/MIRAI does for rust: you add contracts (preconditions, postconditions, and invariants) using 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/ex...

(note: the contracts crate can be used for verifying at runtime as well)

[ Parent | on HN ]

Re:Kind: A Modern Proof Language by touisteur on Thursday August 12, 2021 @07:14AM (#28154801)

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.

[ Parent | on HN ]