Hacker News Reader

Comment by ewuhic | Hacker News Reader

Could anyone suggest a happy path ("zero to hero") book on formal verification, which also does the ecosystem review for the formal verification languages, and then focuses on one, as well as provides the reasoning and mentions tradeoffs for such a choice?

View on HN

https://softwarefoundations.cis.upenn.edu/ is a great zero-to-hero resource (it's what I used), but to my knowledge it doesn't have an ecosystem review in it. It uses Coq, but the first book has been ported to at least Isabelle, if not others.

Also agda: https://plfa.github.io/

I don't think something that specific exists. There are a very large number of formal methods tools, each with different specialties / domains.

For verification with proof assistants, [Software Foundations](https://softwarefoundations.cis.upenn.edu/) and [Concrete Semantics](http://concrete-semantics.org/) are both solid.

For verification via model checking, you can check out [Learn TLA+](https://learntla.com/), and the more theoretical [Specifying Systems](https://lamport.azurewebsites.net/tla/book-02-08-08.pdf).

For more theory, check out [Formal Reasoning About Programs](http://adam.chlipala.net/frap/).

And for general projects look at [F*](https://www.fstar-lang.org/) and [Dafny](https://dafny.org/).

Formal Methods An Appetizer is excellent and has a companion site with toy formal methods implemented in F#: http://www.formalmethods.dk. However, it does not cover proof assistants.

Alternatively you may enjoy these two. The latter is especially thorough, and begins with classical logic:

* Concrete Semantics (Isabelle): http://concrete-semantics.org

* Program = Proof (Agda): https://www.lix.polytechnique.fr/Labo/Samuel.Mimram/teaching...

Types and Programming Languages by Benjamin C. Pierce[0]

[0] https://www.cis.upenn.edu/~bcpierce/tapl/

Since the whole premise here is that formally verifying the properties of programs is equivalent to constructive mathematics, I think you might be asking for too much, modulo your definition of hero.

What do you mean by modulo here?

It means except for X, or disregarding X

If you have a particularly generous definition of hero, then you might not be asking too much

I'm a fan of formal verification of functional programming. It saddens me to say that, in that line of work, hardly anyone speaks English [0], at least not past the front door. The amount of high-horsery and dog-whistling is enough to wear down any regular folk that walks down the path. Maybe it's the nature of the field itself, that those accomplished folks seem to forget they once walked this earth, up right, on two legs.

[0] read: natural language

Agreed! The most famous mathematician in the field told me “I used the first tool I could understand how to write a proof in.” Most he could not!

I was so disgusted by the tutorials for Coq that I wrote my own. It has been reviewed positively on Hacker News before. If you want a look at some of the basics of formal proof and these tools, take a look:

http://michaeldnahas.com/doc/nahas_tutorial.html

There is no such thing as zero to hero for formal methods. It’s a dense and difficult field.

but then, wouldn't the textbook for "MA/CS 301 Introduction to Formal Methods" be the book to read, and you either don't have the prereqs for it (can't understand it maybe because you don't know any functional languages) or it takes you as far as it does and then you decide if that's as far as you want to go?

I am sorry, but my google-foo is lacking to find this book. Could you please name the authors, or just post a link?

> the textbook for "MA/CS 301 Introduction to Formal Methods"

my bad, I was using a "slangy" sort of description to say "shouldn't somebody read the textbook that would be used in a computer science 101 class (or a math 101 class) except not 101 but a hypothetical 3rd level class" so I called it 301. I was asking, "what textbook is used in an upper level undergraduate course on the topic?"

Many American universities use a numbering system of 101 & 102 for the fall and spring term classes somebody majoring in the subject would take, and 201 - 202 for the 2nd year. A CS100-level class would be a lighter survey for somebody who would want to study some CS but not major in it.

Reply on news.ycombinator.com