Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

A Hoare Logic for Rust

ticki.github.io

Post reply on HN
Print view View original

11–20 of 48 posts

Re: A Hoare Logic for Rust

#11

Post by Jtsummers »

cbHXBY1D wrote: post #9

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

Design by Contract: http://c2.com/cgi/wiki?DesignByContract

Which is a key element of the Eiffel language ( https://en.wikipedia.org/wiki/Eiffel_(programming_language) ).

SPARK Ada also includes this concept of pre/post conditions: https://en.wikipedia.org/wiki/SPARK_(programming_language)

I haven't programmed in the latter, but I'd like to. Since I'm often in the maintenance end of the software cycle I don't have much opportunity (professionally) to introduce new languages (new tools, yes, but not new languages).

I have a coworker who thinks we do this with asserts (in C and C++), but it's only half the battle. The asserts only tell us that our exercised version of the program (through our non-comprehensive testing) hasn't failed pre/post-conditions. It's helpful, but not sufficient.

Re: A Hoare Logic for Rust

#13

Post by weinzierl »

dikaiosune wrote: post #4
agentultra wrote: post #2

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

Also the Rust compiler had Typestate analysis at one point of its development. [1]

[1] http://marijnhaverbeke.nl/talks/rustfest_2016/#4

Re: A Hoare Logic for Rust

#14

Post by catnaroek »

Jtsummers wrote: post #11
cbHXBY1D wrote: post #9

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

Design by Contract: http://c2.com/cgi/wiki?DesignByContract Which is a key element of the Eiffel language ( https://en.wikipedia.org/wiki/Eiffel_(programming_language) ). SPARK Ada also includes this concept of pre/post conditions: https://en.wikipedia.org/wiki/SPARK_(programming_language) I haven't programmed in the latter, but I'd like to. Since I'm often in the maintenance end of the software cycle I don't have mu…

Design by contract has nothing to do with formal verification, though.

Re: A Hoare Logic for Rust

#16

Post by Jtsummers »

catnaroek wrote: post #14
Jtsummers wrote: post #11

Earlier quoted context omitted.

Design by Contract: http://c2.com/cgi/wiki?DesignByContract Which is a key element of the Eiffel language ( https://en.wikipedia.org/wiki/Eiffel_(programming_language) ). SPARK Ada also includes this concept of pre/post conditions: https://en.wikipedia.org/wiki/SPARK_(programming_language) I haven't programmed in the latter, but I'd like to. Since I'm often in the maintenance end of the software cycle I don't have mu…

Design by contract has nothing to do with formal verification, though.

Respectfully, I have to disagree. Design by contract is, or can be, a component of formal verification. If it's all you've got, it's probably better than nothing.

Design by contract brings the concept of using preconditions, postconditions, invariants, and other contractual objects into the design and implementation of the software. These are able (depending on implementation) to be analyzed statically by machine or by hand, or dynamically during testing (with some systems the tests can be automatically generated to exercise the contracts). This may not be the limit or ideal of formal verification, but it is certainly a part of it and a good measure forward compared to the typical approaches used in our industry.

EDIT:

Let's settle a pertinent question first: Is Hoare logic a tool/approach for formal verification? If it is, then design by contract (being largely based on the concept of Hoare logic) is also a tool/approach for formal verification.

The potential points of disagreement, as I see them, are that Hoare logic is not a tool for formal verification, or that design by contract is not based on Hoare logic. Is there something else that I've missed or are these the points of disagreement?

Re: A Hoare Logic for Rust

#17

Post by catnaroek »

Jtsummers wrote: post #16
catnaroek wrote: post #14

Earlier quoted context omitted.

Design by contract has nothing to do with formal verification, though.

Respectfully, I have to disagree. Design by contract is, or can be, a component of formal verification. If it's all you've got, it's probably better than nothing. Design by contract brings the concept of using preconditions, postconditions, invariants, and other contractual objects into the design and implementation of the software. These are able (depending on implementation) to be analyzed statically by machine or…

Design by contract forces you to be explicit about your intended preconditions and postconditions. But “intended” isn't the same thing as “actual”. Verification is making sure that the preconditions and postconditions actually hold, in every possible case where the statement (or procedure or whatever) could be reached.

EDIT: Hoare logic is a tool for formal verification, indeed. DbC is not, though.

Re: A Hoare Logic for Rust

#18

Post by Jtsummers »

catnaroek wrote: post #17
Jtsummers wrote: post #16

Earlier quoted context omitted.

Respectfully, I have to disagree. Design by contract is, or can be, a component of formal verification. If it's all you've got, it's probably better than nothing. Design by contract brings the concept of using preconditions, postconditions, invariants, and other contractual objects into the design and implementation of the software. These are able (depending on implementation) to be analyzed statically by machine or…

Design by contract forces you to be explicit about your intended preconditions and postconditions. But “intended” isn't the same thing as “actual”. Verification is making sure that the preconditions and postconditions actually hold, in every possible case where the statement (or procedure or whatever) could be reached. EDIT: Hoare logic is a tool for formal verification, indeed. DbC is not, though.

We're talking around each other. What is your definition of formal verification?

Re: A Hoare Logic for Rust

#19

Post by catnaroek »

Jtsummers wrote: post #18
catnaroek wrote: post #17

Earlier quoted context omitted.

Design by contract forces you to be explicit about your intended preconditions and postconditions. But “intended” isn't the same thing as “actual”. Verification is making sure that the preconditions and postconditions actually hold, in every possible case where the statement (or procedure or whatever) could be reached. EDIT: Hoare logic is a tool for formal verification, indeed. DbC is not, though.

We're talking around each other. What is your definition of formal verification?

Proving that a program meets its specification.
Post reply on HN