3 ms·
There's actually already a library that does what the author is talking about: https://github.com/nrc/libhoare https://github.com/nrc/libhoare They call it "de
by kaiby 7y ago
There's actually already a library that does what the author is talking about: https://github.com/nrc/libhoare https://github.com/nrc/libhoare
They call it "design by contract" rather than "deductive verification" though.
Wish there wouldn't be so many terms for the same thing.
edit: There's also an existing RFC for this: https://github.com/rust-lang/rfcs/issues/1077 https://github.com/rust-lang/rfcs/issues/1077
- rrobukef 7y agoDeductive verification is a large extension of designing by contract: The addition of a SMT solver to verify the contracts at compile time for instance. On the other hand libhoare only adds the contracts as a runtime addition with no mention of formally verifying these. The same with the RFC, it dismissed automatic verification: "Automated proof systems are very hard, especially when AFAIK Rust's type system doesn't even have partial formal proofs yet." This paper shows a similar approach to OP's but applied to Curry: https://arxiv.org/abs/1709.04816 https://arxiv.org/abs/1709.04816. It shows how no formal proofs are needed. However Curry is significantly more pure.