Re:Dafny – A programming language with a program verifier
by qznc on Friday January 20, 2017 @10:33AM
(#13444503)
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...
Re:Dafny – A programming language with a program verifier
by tom_mellior on Friday January 20, 2017 @01:52PM
(#13446034)
My reading of that is that everything is made immutable, at which point aliasing isn't an issue anymore. I might be wrong though.
Re:Dafny – A programming language with a program verifier
by derkha on Friday January 20, 2017 @06:48PM
(#13447888)
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.
Re:Dafny – A programming language with a program verifier
by Sean1708 on Friday January 20, 2017 @10:32AM
(#13444495)
Ownership is used for more than just memory management though, concurrent memory access for example.
Re:Dafny – A programming language with a program verifier
by tom_mellior on Friday January 20, 2017 @10:47AM
(#13444604)
True! I wasn't thinking beyond verification of single-threaded programs, which is hard enough as it is ;-)
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.