[kaiby]

There's actually already a library that does what the author is talking about: 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

[rrobukef]

Deductive 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. It shows how no formal proofs are needed. However Curry is significantly more pure.