4 ms·

The literature on formal methods has evolved a lot. In particular there is some great broad introductory material using either Coq or Isabelle: * https://softw

by nextos 7y ago

The literature on formal methods has evolved a lot. In particular there is some great broad introductory material using either Coq or Isabelle: * https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/ * http://www.concrete-semantics.org/ http://www.concrete-semantics.org/ * http://adam.chlipala.net/frap/ http://adam.chlipala.net/frap/ Even the Little series covers types and proofs now: * https://mitpress.mit.edu/books/little-typer https://mitpress.mit.edu/books/little-typer * https://mitpress.mit.edu/books/little-prover https://mitpress.mit.edu/books/little-prover Plus some topic-specific classics: * https://mitpress.mit.edu/books/principles-model-checking https://mitpress.mit.edu/books/principles-model-checking * https://www.springer.com/gp/book/9783540654100 https://www.springer.com/gp/book/9783540654100 * https://www.cis.upenn.edu/~bcpierce/tapl/ https://www.cis.upenn.edu/~bcpierce/tapl/ And some constructive foundations: * https://www.cambridge.org/core/books/conceptual-mathematics/00772F4CC3D4268200C5EC86B39D415A https://www.cambridge.org/core/books/conceptual-mathematics/... * https://www.cambridge.org/core/books/sets-for-mathematics/E899F592AD8FBA9A550B1ED3E1E61EC3 https://www.cambridge.org/core/books/sets-for-mathematics/E8... * https://www.paultaylor.eu/~pt/prafm/ https://www.paultaylor.eu/~pt/prafm/ * https://www.cs.cmu.edu/~rwh/pfpl/ https://www.cs.cmu.edu/~rwh/pfpl/

nickpsecurity 7y ago
Great set of links. I like to add the easier stuff, too, to get people started. If you like distributed systems, Hillel Wayne's book on TLA+ will let you see how model checking can easily spot errors that are hard to test for: https://www.apress.com/gp/book/9781484238288 https://www.apress.com/gp/book/9781484238288 Spin has been used in similar ways for a long time: https://spinroot.com/ https://spinroot.com/ Alloy is a model checker that has a GUI for exploring models. It's more focused on exploring structures. Their site links to a book, Software Abstractions, that will teach you a lot of concepts without needing a strong, mathematical background. https://alloytools.org/about.html https://alloytools.org/about.html Pamela Zave used both Spin and Alloy to find errors in real-world protocols: http://www.pamelazave.com/compare.html http://www.pamelazave.com/compare.html If focus is programming (esp low-level), SPARK Ada lets programmers annotate code with the expected behavior before that's fed into provers that confirm or refute the code operates that way in all situations. Barnes and Barnes wrote a nice book teaching both it and Praxis' Correct-by-Construction method for software development: https://www.betterworldbooks.com/product/detail/High-Integrity-Software--The-Spark-Approach-to-Safety-and-Security-9780321136169 https://www.betterworldbooks.com/product/detail/High-Integri... Many people don't make it through the stuff teaching formal proof in Coq and so on. It's really hard with few gains along the way. TLA+, SPIN, Alloy, and SPARK Ada are much more accessible with a higher work-to-reward ratio. Those easier results might justify further investment in learning the hard stuff. Those wondering about how formal methods are used in a lot of situations might like our list on Lobsters. We have a number of professionals and enthusiasts there who stay posting both historically significant and cutting-edge work. https://lobste.rs/t/formalmethods https://lobste.rs/t/formalmethods
- touisteur 7y ago
  And with SPARK if you want to dive into manual proof of a property (usually because SPARK & Why3 and all the SMT solvers can't manage and you don't have some appropriate lemmas) with Coq or Isabelle. Some introduction https://blog.adacore.com/using-coq-to-verify-spark-2014-code https://blog.adacore.com/using-coq-to-verify-spark-2014-code (from 2014, so probably much improved since). And some examples : http://docs.adacore.com/spark2014-docs/html/ug/gnatprove_by_example/manual_proof.html http://docs.adacore.com/spark2014-docs/html/ug/gnatprove_by_... Not the best way to learn manual proof, but I've seen it used very efficiently. But then if course you're faced with the difficulty of increasing automation : the more you automate, the more it is difficult to have the 'muscle memory' (and lower cognitive load) that you get when flexing the manual proof often...
  - nickpsecurity 7y ago
    Even that is getting automation as I long ago predicted. I think the SPARK-type proofs will be easier to automate this way, too, since they're more mechanical. https://blog.acolyer.org/2019/08/23/learning-to-prove-theorems-via-interacting-with-proof-assistants/ https://blog.acolyer.org/2019/08/23/learning-to-prove-theore...
Gajurgensen 7y ago
I highly recommend people interested in Coq start with Pierce's Logical Foundations. It is by far the most accessible introduction to Coq I've found. I'm working through Chlipala's books next. CPDT is a great deep-dive into more advanced use cases of Coq as well as its theoretical underpinnings. I'll be taking a class this semester based on FRAP, my understanding is it hits those formal methods and language topics without specifically emphasizing Coq, except for the exercises. As an aside, since Coq is the only theorem proving language I know well, I am curious what the pros/cons are as compared to Isabelle/HOL, F*, Lean, etc. Coq has been around for a while, but I keep seeing new theorem provers pop up. What are the alleged weaknesses of Coq that other languages are trying to fix?
- Cladode 7y ago
  pros/cons The main issue is proof automation. Curry-Howard based provers (Coq, Agda, Lean etc) are nice for teaching but if you want to get work done (e.g. you want to verify an OS kernel), you need to automate as much as possible. Isabelle/HOL currently has by far the most powerful automation. This is partly because, like Coq, it is an old system (unlike Lean and Agda) and lots of automation has been built in the past, but also because a lot of automation is much easier to adapt to provers based on classical logic (as opposed to the constructive logics that Curry-Howard needs (yes, I know that classical reasoning can be done within constructive logic)). Adapting proof automation that has been available for a while for Isabelle/HOL to Curry-Howard is at least in parts an open research problem. Lean has been created in parts because of the urgency of given Curry-Howard systems much better proof automation. There is an additional dimension which is strength of the logic at hand. The logics Coq, Lean et al are based on are more expressive in various dimensions. Whether that's relevant to your use case depends on what kind of maths you are trying to formalise. If it is higher category theory, it matters a great deal, for program verification it tends not to be important b/c most program verification can be done in rather weak logics.
  - kd0amg 7y ago
    How does being classical help with automation? I'm more familiar with ACL2, which seems to gain a lot more on the automation front from being first-order than from anything else (though it has sort of a weird take on the excluded middle).
pron 7y ago
This is more programming language theory, or, rather the PL-theory portion of formal methods, which is a small portion of formal methods research. Most formal methods research these days focuses on sound static analysis, model checking and concolic testing, techniques that are showing better scalability than the deductive methods favored by PL theorists.
- nextos 7y ago
  I agree, but Concrete Semantics and the other 2 equivalent references are a general introduction to everything. Yes, they use theorem provers, but proofs are optional and not required to follow the material. And they do cover those topics you mention.

by nextos 7y ago

nickpsecurity 7y ago

Great set of links. I like to add the easier stuff, too, to get people started. If you like distributed systems, Hillel Wayne's book on TLA+ will let you see how model checking can easily spot errors that are hard to test for: https://www.apress.com/gp/book/9781484238288 https://www.apress.com/gp/book/9781484238288 Spin has been used in similar ways for a long time: https://spinroot.com/ https://spinroot.com/ Alloy is a model checker that has a GUI for exploring models. It's more focused on exploring structures. Their site links to a book, Software Abstractions, that will teach you a lot of concepts without needing a strong, mathematical background. https://alloytools.org/about.html https://alloytools.org/about.html Pamela Zave used both Spin and Alloy to find errors in real-world protocols: http://www.pamelazave.com/compare.html http://www.pamelazave.com/compare.html If focus is programming (esp low-level), SPARK Ada lets programmers annotate code with the expected behavior before that's fed into provers that confirm or refute the code operates that way in all situations. Barnes and Barnes wrote a nice book teaching both it and Praxis' Correct-by-Construction method for software development: https://www.betterworldbooks.com/product/detail/High-Integrity-Software--The-Spark-Approach-to-Safety-and-Security-9780321136169 https://www.betterworldbooks.com/product/detail/High-Integri... Many people don't make it through the stuff teaching formal proof in Coq and so on. It's really hard with few gains along the way. TLA+, SPIN, Alloy, and SPARK Ada are much more accessible with a higher work-to-reward ratio. Those easier results might justify further investment in learning the hard stuff. Those wondering about how formal methods are used in a lot of situations might like our list on Lobsters. We have a number of professionals and enthusiasts there who stay posting both historically significant and cutting-edge work. https://lobste.rs/t/formalmethods https://lobste.rs/t/formalmethods

touisteur 7y ago
And with SPARK if you want to dive into manual proof of a property (usually because SPARK & Why3 and all the SMT solvers can't manage and you don't have some appropriate lemmas) with Coq or Isabelle. Some introduction https://blog.adacore.com/using-coq-to-verify-spark-2014-code https://blog.adacore.com/using-coq-to-verify-spark-2014-code (from 2014, so probably much improved since). And some examples : http://docs.adacore.com/spark2014-docs/html/ug/gnatprove_by_example/manual_proof.html http://docs.adacore.com/spark2014-docs/html/ug/gnatprove_by_... Not the best way to learn manual proof, but I've seen it used very efficiently. But then if course you're faced with the difficulty of increasing automation : the more you automate, the more it is difficult to have the 'muscle memory' (and lower cognitive load) that you get when flexing the manual proof often...
- nickpsecurity 7y ago
  Even that is getting automation as I long ago predicted. I think the SPARK-type proofs will be easier to automate this way, too, since they're more mechanical. https://blog.acolyer.org/2019/08/23/learning-to-prove-theorems-via-interacting-with-proof-assistants/ https://blog.acolyer.org/2019/08/23/learning-to-prove-theore...

Gajurgensen 7y ago

I highly recommend people interested in Coq start with Pierce's Logical Foundations. It is by far the most accessible introduction to Coq I've found. I'm working through Chlipala's books next. CPDT is a great deep-dive into more advanced use cases of Coq as well as its theoretical underpinnings. I'll be taking a class this semester based on FRAP, my understanding is it hits those formal methods and language topics without specifically emphasizing Coq, except for the exercises. As an aside, since Coq is the only theorem proving language I know well, I am curious what the pros/cons are as compared to Isabelle/HOL, F*, Lean, etc. Coq has been around for a while, but I keep seeing new theorem provers pop up. What are the alleged weaknesses of Coq that other languages are trying to fix?

Cladode 7y ago
pros/cons The main issue is proof automation. Curry-Howard based provers (Coq, Agda, Lean etc) are nice for teaching but if you want to get work done (e.g. you want to verify an OS kernel), you need to automate as much as possible. Isabelle/HOL currently has by far the most powerful automation. This is partly because, like Coq, it is an old system (unlike Lean and Agda) and lots of automation has been built in the past, but also because a lot of automation is much easier to adapt to provers based on classical logic (as opposed to the constructive logics that Curry-Howard needs (yes, I know that classical reasoning can be done within constructive logic)). Adapting proof automation that has been available for a while for Isabelle/HOL to Curry-Howard is at least in parts an open research problem. Lean has been created in parts because of the urgency of given Curry-Howard systems much better proof automation. There is an additional dimension which is strength of the logic at hand. The logics Coq, Lean et al are based on are more expressive in various dimensions. Whether that's relevant to your use case depends on what kind of maths you are trying to formalise. If it is higher category theory, it matters a great deal, for program verification it tends not to be important b/c most program verification can be done in rather weak logics.
- kd0amg 7y ago
  How does being classical help with automation? I'm more familiar with ACL2, which seems to gain a lot more on the automation front from being first-order than from anything else (though it has sort of a weird take on the excluded middle).

pron 7y ago

This is more programming language theory, or, rather the PL-theory portion of formal methods, which is a small portion of formal methods research. Most formal methods research these days focuses on sound static analysis, model checking and concolic testing, techniques that are showing better scalability than the deductive methods favored by PL theorists.

nextos 7y ago
I agree, but Concrete Semantics and the other 2 equivalent references are a general introduction to everything. Yes, they use theorem provers, but proofs are optional and not required to follow the material. And they do cover those topics you mention.