3 ms·

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 mains

by qznc 10y ago

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.

tom_mellior 10y ago
> 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.
- Sean1708 10y ago
  Ownership is used for more than just memory management though, concurrent memory access for example.
  - tom_mellior 10y ago
    True! I wasn't thinking beyond verification of single-threaded programs, which is hard enough as it is ;-)
- qznc 10y ago
  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-binary-search.html https://kha.github.io/2016/07/22/formally-verifying-rusts-bi...
  - tom_mellior 10y ago
    My reading of that is that everything is made immutable, at which point aliasing isn't an issue anymore. I might be wrong though.
    - derkha 10y ago
      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.

by qznc 10y ago

tom_mellior 10y ago

> 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.

Sean1708 10y ago
Ownership is used for more than just memory management though, concurrent memory access for example.
- tom_mellior 10y ago
  True! I wasn't thinking beyond verification of single-threaded programs, which is hard enough as it is ;-)
qznc 10y ago
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-binary-search.html https://kha.github.io/2016/07/22/formally-verifying-rusts-bi...
- tom_mellior 10y ago
  My reading of that is that everything is made immutable, at which point aliasing isn't an issue anymore. I might be wrong though.
  - derkha 10y ago
    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.