Kind: A Modern Proof Language

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 ]