[deleted]
A Hoare Logic for Rust
41–48 of 48 posts
Re: A Hoare Logic for Rust
#42Very broken for me on Chrome. All the equations are randomly overlapping words. (Version 53.0.2785.116 m (64-bit))
Adblock Pro did that for me, disabling it on the website fixes things
Re: A Hoare Logic for Rust
#43Heh, just realized my https://github.com/Ericson2314/a-stateful-mir-for-rust is a lot more like separation logic than I knew.
Re: A Hoare Logic for Rust
#44Very cool. I've long that that having formal program verification built in to a language and run as part of the compiler is the way forward. Giving the pre and post-conditions for a function is much more reasonable than dropping down to a verification tool like Coq or TLA+. I know that AWS uses TLA+ to reason about the correctness of algorithms.
> Giving the pre and post-conditions for a function is much more reasonable than dropping down to a verification tool like Coq or TLA+
Reasonable for what? The design hypothesis behind a high-level specification/verification tool like TLA+ is that no language is currently capable of being reasoned-about in such a way that large, complex applications can be verified affordably. So far, this hypothesis holds. Language-level verification is therefore valuable when you either need to verify very local properties (pre/post conditions of a single subroutine, that is very important and/or tricky) or you need to do full end-to-end verification, in which case you will be able to verify only relatively small and simplified programs (like seL4 or CompCert) and at a very high cost (reasonable for high-assurance software only). So language-level verification and high-level specification and verification are currently useful for very different things.
Re: A Hoare Logic for Rust
#45Nice. It makes sense to try to formalize the semantics of Rust's new intermediate representation, MIR. It's much easier to get unambiguous semantics at that level. All name issues such as shadowing are gone, type issues have been resolved, and operations are machine-level unambiguous (not "+", "32 bit unsigned add"). An old project I worked on, the Pascal-F verifier,[1] from the early 1980s, worked in a similar way.…
Thanks for this.
Too much work in verification has been done by people who wanted to publish math papers, not kill program bugs. This is about creating bug-free code. I think people will get this now,
This might be right, but when I go areading I still find all the maths-orriented stuff.
Re: A Hoare Logic for Rust
#46Very nice! Is work being done to produce a formal, verifiable specification? edit : I'm particularly interested in formal specifications and their use in open source software.
I know of a few efforts to better specify Rust in addition to ticki's (OP): * https://github.com/nikomatsakis/rust-memory-model * http://plv.mpi-sws.org/rustbelt/ * https://kha.github.io/2016/07/22/formally-verifying-rusts-bi... The first isn't using formal methods AFAIK, the second is, and the third is as well, but I think they're targeting safe code only.
Rustbelt targets unsafe and safe code. In addition, it will also deal with concurrency (incl. weak memory).
Disclaimer: I am affiliated with the project.
Re: A Hoare Logic for Rust
#47Earlier quoted context omitted.
> In DbC, you have preconditions and postconditions, but no means whatsoever to actually prove that, whenever the procedure's initial state meets the precondition, its final state will meet the postcondition. Except many implementations of design by contract execute the postcondition check and raise an exception if it's not satisfied, so I don't think your statement is correct.
The very reason why you need to raise the exception is because the postcondition doesn't hold. The point to verification is to make sure the postcondition holds . So I stand by my original assertion: DbC isn't verification.
If I were to categorize it, I'd call DbC formal specification that, combined with Eiffel or SPARK tools, can be used to verify that interfaces or code maintain those specific properties. It's a partial form of formal specification and verification that's still useful.
It doesn't have to be fully specified or proven to count as formal verification. Partial verification is a thriving field.
Re: A Hoare Logic for Rust
#48Earlier quoted context omitted.
The very reason why you need to raise the exception is because the postcondition doesn't hold. The point to verification is to make sure the postcondition holds . So I stand by my original assertion: DbC isn't verification.
If I were to categorize it, I'd call DbC formal specification that, combined with Eiffel or SPARK tools, can be used to verify that interfaces or code maintain those specific properties. It's a partial form of formal specification and verification that's still useful. It doesn't have to be fully specified or proven to count as formal verification. Partial verification is a thriving field.
Yep, that's perfectly reasonable.