Hacker News Reader

Comment by qznc | Hacker News Reader

It is a gradual range from untyped (assembly) to proof-anything (Isabelle, Coq). The more interesting question is: Where are the sweet spots?

The current mainstream (Java,C++,etc) form a big cluster "sweetrange" of roughly equivalent type safety. Rust with its ownership type system goes one step towards more proofs. ATS is even further. Agda and Idris want to be useable programming languages while providing as much proof as possible. Isabelle can generate code, but is also used as just a theorem prover.

View on HN

> Rust with its ownership type system goes one step towards more proofs.

Does it really, though? The ownership system only talks about ownership, which you only need to reason about due to the artificial choice of avoiding garbage collection. So yes, you get closer to proofs, but only to proofs of properties that are not necessary to prove for Java, say.

You might use the ownership and lifetime system to derive must-not-alias guarantees that might help with some verification tasks, but I'm not sure how much it would help.

I'd love to see a deductive verification system for Rust, but I wouldn't expect it to be the silver bullet for verification.

Ownership is used for more than just memory management though, concurrent memory access for example.

True! I wasn't thinking beyond verification of single-threaded programs, which is hard enough as it is ;-)

There is a convert-Rust-to-Lean-for-verification project. The not-aliasing guarantees did help tremendously there.

https://kha.github.io/2016/07/22/formally-verifying-rusts-bi...

My reading of that is that everything is made immutable, at which point aliasing isn't an issue anymore. I might be wrong though.

Author of that project here, it's the other way around - I'm using the absence oft aliasing to turn mutable Rust code immutable, which I can then embed in Lean. But you're right that ownership (ie, affine types) per se doesn't help.

Reply on news.ycombinator.com