6 ms·

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

by ewuhic 3y ago

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?

miloignis 3y ago
https://softwarefoundations.cis.upenn.edu/ 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.
- blueberry87 3y ago
  Also agda: https://plfa.github.io/ https://plfa.github.io/
noqc 3y ago
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.
- bruce343434 3y ago
  What do you mean by modulo here?
  - tux3 3y ago
    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
rsrsrs86 3y ago
There is no such thing as zero to hero for formal methods. It’s a dense and difficult field.
- fsckboy 3y ago
  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?
  - ewuhic 3y ago
    I am sorry, but my google-foo is lacking to find this book. Could you please name the authors, or just post a link?
    - fsckboy 3y ago
      > 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.
jurynulifcation 3y ago
Types and Programming Languages by Benjamin C. Pierce[0] [0] https://www.cis.upenn.edu/~bcpierce/tapl/ https://www.cis.upenn.edu/~bcpierce/tapl/
nextos 3y ago
Formal Methods An Appetizer is excellent and has a companion site with toy formal methods implemented in F#: http://www.formalmethods.dk 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 http://concrete-semantics.org * Program = Proof (Agda): https://www.lix.polytechnique.fr/Labo/Samuel.Mimram/teaching/INF551/course.pdf https://www.lix.polytechnique.fr/Labo/Samuel.Mimram/teaching...
amw-zero 3y ago
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/ https://softwarefoundations.cis.upenn.edu/) and [Concrete Semantics](http://concrete-semantics.org/ http://concrete-semantics.org/) are both solid. For verification via model checking, you can check out [Learn TLA+](https://learntla.com/ https://learntla.com/), and the more theoretical [Specifying Systems](https://lamport.azurewebsites.net/tla/book-02-08-08.pdf https://lamport.azurewebsites.net/tla/book-02-08-08.pdf). For more theory, check out [Formal Reasoning About Programs](http://adam.chlipala.net/frap/ http://adam.chlipala.net/frap/). And for general projects look at [F*](https://www.fstar-lang.org/ https://www.fstar-lang.org/) and [Dafny](https://dafny.org/ https://dafny.org/).
penguin_booze 3y ago
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
- mdnahas 3y ago
  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 http://michaeldnahas.com/doc/nahas_tutorial.html

by ewuhic 3y ago

miloignis 3y ago

https://softwarefoundations.cis.upenn.edu/ 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.

blueberry87 3y ago
Also agda: https://plfa.github.io/ https://plfa.github.io/

noqc 3y ago

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.

bruce343434 3y ago
What do you mean by modulo here?
- tux3 3y ago
  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

rsrsrs86 3y ago

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

fsckboy 3y ago
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?
- ewuhic 3y ago
  I am sorry, but my google-foo is lacking to find this book. Could you please name the authors, or just post a link?
  - fsckboy 3y ago
    > 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.

jurynulifcation 3y ago

Types and Programming Languages by Benjamin C. Pierce[0] [0] https://www.cis.upenn.edu/~bcpierce/tapl/ https://www.cis.upenn.edu/~bcpierce/tapl/

nextos 3y ago

Formal Methods An Appetizer is excellent and has a companion site with toy formal methods implemented in F#: http://www.formalmethods.dk 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 http://concrete-semantics.org * Program = Proof (Agda): https://www.lix.polytechnique.fr/Labo/Samuel.Mimram/teaching/INF551/course.pdf https://www.lix.polytechnique.fr/Labo/Samuel.Mimram/teaching...

amw-zero 3y ago

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/ https://softwarefoundations.cis.upenn.edu/) and [Concrete Semantics](http://concrete-semantics.org/ http://concrete-semantics.org/) are both solid. For verification via model checking, you can check out [Learn TLA+](https://learntla.com/ https://learntla.com/), and the more theoretical [Specifying Systems](https://lamport.azurewebsites.net/tla/book-02-08-08.pdf https://lamport.azurewebsites.net/tla/book-02-08-08.pdf). For more theory, check out [Formal Reasoning About Programs](http://adam.chlipala.net/frap/ http://adam.chlipala.net/frap/). And for general projects look at [F*](https://www.fstar-lang.org/ https://www.fstar-lang.org/) and [Dafny](https://dafny.org/ https://dafny.org/).

penguin_booze 3y ago

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

mdnahas 3y ago
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 http://michaeldnahas.com/doc/nahas_tutorial.html