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

21–30 of 48 posts

Re: A Hoare Logic for Rust

#21

Post by catnaroek »

Jtsummers wrote: post #20
catnaroek wrote: post #19

Earlier quoted context omitted.

Proving that a program meets its specification.

Is Hoare logic a tool in that process?

Yes. Hoare logic's inference rules define which Hoare triples can be “legally” derived. The programmer's task isn't only to provide a Hoare triple (which by itself is just an assertion that a program meets a specification), but also to provide a derivation of that triple (the actual proof of the assertion). Design by contract is akin to giving a Hoare triple, but never giving its derivation.

Re: A Hoare Logic for Rust

#22

Post by Jtsummers »

catnaroek wrote: post #21
Jtsummers wrote: post #20

Earlier quoted context omitted.

Is Hoare logic a tool in that process?

Yes. Hoare logic's inference rules define which Hoare triples can be “legally” derived. The programmer's task isn't only to provide a Hoare triple (which by itself is just an assertion that a program meets a specification), but also to provide a derivation of that triple (the actual proof of the assertion). Design by contract is akin to giving a Hoare triple, but never giving its derivation.

Design by contract, is it based or not based on Hoare logic?

Re: A Hoare Logic for Rust

#23

Post by catnaroek »

Jtsummers wrote: post #22
catnaroek wrote: post #21

Earlier quoted context omitted.

Yes. Hoare logic's inference rules define which Hoare triples can be “legally” derived. The programmer's task isn't only to provide a Hoare triple (which by itself is just an assertion that a program meets a specification), but also to provide a derivation of that triple (the actual proof of the assertion). Design by contract is akin to giving a Hoare triple, but never giving its derivation.

Design by contract, is it based or not based on Hoare logic?

It's not. 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.

Re: A Hoare Logic for Rust

#25

Post by [deleted] »

catnaroek wrote: post #23
Jtsummers wrote: post #22

Earlier quoted context omitted.

Design by contract, is it based or not based on Hoare logic?

It's not. 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.

[deleted]

Re: A Hoare Logic for Rust

#26

Post by [deleted] »

catnaroek wrote: post #23
Jtsummers wrote: post #22

Earlier quoted context omitted.

Design by contract, is it based or not based on Hoare logic?

It's not. 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.

[deleted]

Re: A Hoare Logic for Rust

#27

Post by Jtsummers »

catnaroek wrote: post #23
Jtsummers wrote: post #22

Earlier quoted context omitted.

Design by contract, is it based or not based on Hoare logic?

It's not. 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.

Well, I've found the point disagreement.

So design by contract, based on Hoare logic, applied in languages like SPARK Ada and Eiffel, produces statements that are unverifiable.

But Hoare logic, a thing without an executable implementation, produces statements which are verifiable.

Re: A Hoare Logic for Rust

#28

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.

My last statement, since you've edited several of your comments without marking them as edited which makes this conversation, well, not an accurate account of our dialogue. Thanks for that.

You state that design by contract has nothing to do with formal verification. You also later said that Hoare logic is a tool for formal verification. Design by contract is an implementation/application of Hoare logic. Ergo, it has something to do with formal verification.

I've never said it is formal verification, I've only said that it is part of it. It requires tooling and proper application for it to be useful/correct/effective. But that's true of everything in formal verification.

Re: A Hoare Logic for Rust

#29

Post by paulddraper »

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.

Design by contact is more or less a prerequisite to formal verification.

If you don't have a well-defined contact, you won't be able to verify that context is adhered to.

Re: A Hoare Logic for Rust

#30

Post by kwantam »

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.

There's a forthcoming paper at PLAS (co-located with ACM CCS, in late October) that applies formal reasoning to a Rust-like type system.

The contribution here is a formalization of borrowing and ownership semantics very close to Rust's, plus a sketch of how one would prove that these semantics give memory safety. The techniques can probably be adapted to an analysis of Rust itself.

Benitez, S. "Rusty Types for Solid Safety." ACM PLAS 2016. https://sergio.bz/docs/rusty-types-2016.pdf

(Full disclosure: Sergio and I are colleagues.)

Post reply on HN