5 ms·

I'd recommend people interested in learning formal methods do not start with things such as Coq or Isabelle/HOL. Most people find the process of learning or usi

I'd recommend people interested in learning formal methods do not start with things such as Coq or Isabelle/HOL. Most people find the process of learning or using those so difficult that they quit with a potentially-permanent aversion to the term formal verification. In engineering, it's often advised to use best tool for the job esp with highest ROI. So, if you're interested in formal methods, I strongly encourage you to start with so-called, lightweight methods that give a lot of return for little investment. They teach you how abstract specifications with tool-assisted reasoning can quickly catch deep errors tests often won't. Two of those with lots of benefit in realistic projects are Alloy Analyzer (esp for structure) and TLA+/PlusCal (esp for order): http://alloy.mit.edu/ http://alloy.mit.edu/ https://learntla.com/introduction/ https://learntla.com/introduction/ These are immediately useful. Especially in distributed systems for TLA+. Then, you get a book such as Chlipala's Certified Programming with Dependent Types or Pierce et al's Software Foundations. Chlipala is also doing a new one called "Formal Reasoning About Programs." You can try to use those to get some elementary stuff done with the heavyweight methods. It will probably take you 1-2 years to get proficient enough for real stuff. Two outcomes are common: 1. You don't make it. Don't get mad: most don't even when they're smart. Good news is you enjoyed lighter stuff that you'll probably continue to apply and expand on for rest of your career. If other users are lucky, you might have run into their limitations enough to start improving the tooling, documentation, or something else. Those will get better since you learned them but avoided heavyweight stuff. 2. You made it! Now, best result for us IT folks is you apply your skills to real-world software formally-verifying useful algorithms, protocols, compilers, OS's, and so on. For inspiration, be sure to look at CRYPTOL, miTLS, CompCert, CakeML, RockSalt, seL4 or VAMOS, Verdi, verified garbage collectors, foundational backing of static analyzers like Verasco, tools with automation such as SPARK Ada, ACL2 for hardware, and maybe rewriting-based stuff like C semantics in K Framework. If you can understand heavyweight verification, then apply your knowledge to more stuff like that since you'll (a) possibly be having real-world impact and (b) be doing work challenging enough that you can be very proud of your successes.

kyberias 9y ago
What an inspiring comment filled with useful information! Thank you, sir.
pron 9y ago
The main advantage of TLA+/Alloy over Isabelle/Coq/Lean for beginners (in general, they make completely different tradeoffs [1]) is that because they have automatic verification tools (only, in Alloy, and in addition to an interactive proof assistant in TLA+), they allow separating the much more important skill of formal specification from the less important skill of writing formal proofs. In TLA+, you can learn specification first, and then, if you want, learn writing proofs. One of the annoyances of learning Coq/Lean, is that you must learn specification and proof, together, right from the get go, before you even understand what formal logic is. Indeed, formal logic serves two different purposes: formal specification (description) and formal proof. The first can be immensely useful, even without the other. One problem with Alloy, for someone who wants to learn logic, is that it uses a completely different notation from ordinary mathematical notation. OTOH, TLA+ is probably the formal tool that uses the notation most similar to ordinary mathematical notation (more so than Coq, Lean, or Isabelle), and formal proofs (if you want to write them -- you don't have to), that are by far the most readable. [1]: https://news.ycombinator.com/item?id=15777748 https://news.ycombinator.com/item?id=15777748
- auggierose 9y ago
  Actually, you should distinguish Coq from Isabelle in that respect. In Isabelle it is MUCH more feasible to separate specification and automation.
Karrot_Kream 9y ago
Heavyweight formal methods, such as Coq and Isabelle, take quite a bit of time to get into. You generally have to build up semantics of your domain and go up from there. Coq is trying to fix this by building up their tactics libraries and other things, but it can still be a slog.
dbcurtis 9y ago
Inspired by your post, I spent a few minutes reading the Allow web site. I'm wondering exactly how to benefit from Alloy? I have a problem that involves multiple interacting state machines communicating over protocols that I don't necessarily control, over unreliable network connections. Lots of retry/recovery arcs. So assuming I could specify this system with Alloy, what would I learn? I'm guessing I would at least detect gaps in the protocols and missing error recovery arcs in state machines. But that doesn't yield a correct implementation... it might help me fill in gaps in the validation test coverage space. Is this what I should expect?
- tel 9y ago
  Most practically: your personal knowledge of the system will grow tremendously through the process of trying to formalize it and debug the errors you encounter. It's likely that basic assumptions you have about the protocol are false and that real bugs arise due to these subtle imperfections. Some formal system technologies let you "extract" algorithms into other languages. Model checkers like Alloy don't. What you take away is what you learn and what you can use of that learning to convince others. A good concrete takeaway would be information you could use to design a test suite that breaks the system even where others believe it to be solid.
  - dbcurtis 9y ago
    My backround in hardware and software validation is long and deep, so I clearly see the benefit of getting information about the test space that needs to be covered. Still, it seems like it ought to be possible to do some kind of automated test stimulus generation using what Alloy already does. I am imagining a machine-readable report in some format that is easy to feed into a problem-specific test generator script. In a past life, I worked on automatic test pattern generation for sequential logic circuits. Which, if you want to tilt at windmills for little $return (1), is as good a pursuit as any. But it strikes me that this is a very similar problem. Given a description of a state space, create stimulus that covers it, sensitizing all the logic paths in a way that produces an observable result that differs from expectations. (1) The central lesson of trying to sell test: Electronic Design Automation dollars are like western US water law, the first to divert wins. In the case of EDA, the up-front design tools get all the dollars, and there is hardly a trickle of money left by the time it reaches test phase.
marco_salvatori 9y ago
One can also download the TLA+ book and the TLA+ hyperbook from Leslie Lamport' TLA home page https://lamport.azurewebsites.net/tla/tla.html https://lamport.azurewebsites.net/tla/tla.html Both are very useful resources and for those interested in learning I would recommend going through both together letting the book fill in the detail where the hyperbook leaves you wanting more information. The hyperbook concetrates on PlusCal, which is a higher level interface to the TLA language, while the TLA book is all in the TLA language itself. I find,in practice,that the TLA language is what I am more comfortable writing specifications in. I find it clearer and as essentially standard mathematical notation its one less thing to learn. I believe Leslie encourages engineers to use PlusCal as being more user friendly. Once one has worked though the specification course in the hyperbook, one should be able to apply TLA to real problems in any event driven system. (Sequential problems can also be modeled though). The primary hurdle in getting to applications will probably be coming to the understanding that modeling work happens at a much higher level of abstraction than programming, and that ones insticts as programmers, to get into detail, are not correct. The benefits are two fold. Modeling a system before it's built forces one to abstract, clarify and simplify ones approach. The second benefit is that the model checker will find all the corner cases and complexity that one missed in the design. If one does a good translation from the model to code from there, then to a first approximation the code is bug free. As a bonus, later, when one goes back to code that has a spec, the spec is a nice summary of what has been coded (becase you forgot) and one can modify, and verify the spec before one updates the code.
charlysl 9y ago
Very helpful post. I decided to learn Alloy inspired by the excellent OCW course by its author Prof. Daniel Jackson, "Elements of Software Construction" 2008 [1], where it is introduced in the very interesting OO lecture. My plan is to learn some logic first though, specially relational logic, from Stanforfd's "Introduction to Logic" [2], which I am enjoying. There is also an Alloy book, with many examples like OO design and state machine based messaging protocols. [1] https://ocw.mit.edu/courses/electrical-engineering-and-computer-science/6-005-elements-of-software-construction-fall-2008 https://ocw.mit.edu/courses/electrical-engineering-and-compu... [2] http://intrologic.stanford.edu/lessons/lessons.html http://intrologic.stanford.edu/lessons/lessons.html

kyberias 9y ago

What an inspiring comment filled with useful information! Thank you, sir.

pron 9y ago

The main advantage of TLA+/Alloy over Isabelle/Coq/Lean for beginners (in general, they make completely different tradeoffs [1]) is that because they have automatic verification tools (only, in Alloy, and in addition to an interactive proof assistant in TLA+), they allow separating the much more important skill of formal specification from the less important skill of writing formal proofs. In TLA+, you can learn specification first, and then, if you want, learn writing proofs. One of the annoyances of learning Coq/Lean, is that you must learn specification and proof, together, right from the get go, before you even understand what formal logic is. Indeed, formal logic serves two different purposes: formal specification (description) and formal proof. The first can be immensely useful, even without the other. One problem with Alloy, for someone who wants to learn logic, is that it uses a completely different notation from ordinary mathematical notation. OTOH, TLA+ is probably the formal tool that uses the notation most similar to ordinary mathematical notation (more so than Coq, Lean, or Isabelle), and formal proofs (if you want to write them -- you don't have to), that are by far the most readable. [1]: https://news.ycombinator.com/item?id=15777748 https://news.ycombinator.com/item?id=15777748

auggierose 9y ago
Actually, you should distinguish Coq from Isabelle in that respect. In Isabelle it is MUCH more feasible to separate specification and automation.

Karrot_Kream 9y ago

Heavyweight formal methods, such as Coq and Isabelle, take quite a bit of time to get into. You generally have to build up semantics of your domain and go up from there. Coq is trying to fix this by building up their tactics libraries and other things, but it can still be a slog.

dbcurtis 9y ago

Inspired by your post, I spent a few minutes reading the Allow web site. I'm wondering exactly how to benefit from Alloy? I have a problem that involves multiple interacting state machines communicating over protocols that I don't necessarily control, over unreliable network connections. Lots of retry/recovery arcs. So assuming I could specify this system with Alloy, what would I learn? I'm guessing I would at least detect gaps in the protocols and missing error recovery arcs in state machines. But that doesn't yield a correct implementation... it might help me fill in gaps in the validation test coverage space. Is this what I should expect?

tel 9y ago
Most practically: your personal knowledge of the system will grow tremendously through the process of trying to formalize it and debug the errors you encounter. It's likely that basic assumptions you have about the protocol are false and that real bugs arise due to these subtle imperfections. Some formal system technologies let you "extract" algorithms into other languages. Model checkers like Alloy don't. What you take away is what you learn and what you can use of that learning to convince others. A good concrete takeaway would be information you could use to design a test suite that breaks the system even where others believe it to be solid.
- dbcurtis 9y ago
  My backround in hardware and software validation is long and deep, so I clearly see the benefit of getting information about the test space that needs to be covered. Still, it seems like it ought to be possible to do some kind of automated test stimulus generation using what Alloy already does. I am imagining a machine-readable report in some format that is easy to feed into a problem-specific test generator script. In a past life, I worked on automatic test pattern generation for sequential logic circuits. Which, if you want to tilt at windmills for little $return (1), is as good a pursuit as any. But it strikes me that this is a very similar problem. Given a description of a state space, create stimulus that covers it, sensitizing all the logic paths in a way that produces an observable result that differs from expectations. (1) The central lesson of trying to sell test: Electronic Design Automation dollars are like western US water law, the first to divert wins. In the case of EDA, the up-front design tools get all the dollars, and there is hardly a trickle of money left by the time it reaches test phase.

marco_salvatori 9y ago

One can also download the TLA+ book and the TLA+ hyperbook from Leslie Lamport' TLA home page https://lamport.azurewebsites.net/tla/tla.html https://lamport.azurewebsites.net/tla/tla.html Both are very useful resources and for those interested in learning I would recommend going through both together letting the book fill in the detail where the hyperbook leaves you wanting more information. The hyperbook concetrates on PlusCal, which is a higher level interface to the TLA language, while the TLA book is all in the TLA language itself. I find,in practice,that the TLA language is what I am more comfortable writing specifications in. I find it clearer and as essentially standard mathematical notation its one less thing to learn. I believe Leslie encourages engineers to use PlusCal as being more user friendly. Once one has worked though the specification course in the hyperbook, one should be able to apply TLA to real problems in any event driven system. (Sequential problems can also be modeled though). The primary hurdle in getting to applications will probably be coming to the understanding that modeling work happens at a much higher level of abstraction than programming, and that ones insticts as programmers, to get into detail, are not correct. The benefits are two fold. Modeling a system before it's built forces one to abstract, clarify and simplify ones approach. The second benefit is that the model checker will find all the corner cases and complexity that one missed in the design. If one does a good translation from the model to code from there, then to a first approximation the code is bug free. As a bonus, later, when one goes back to code that has a spec, the spec is a nice summary of what has been coded (becase you forgot) and one can modify, and verify the spec before one updates the code.

charlysl 9y ago

Very helpful post. I decided to learn Alloy inspired by the excellent OCW course by its author Prof. Daniel Jackson, "Elements of Software Construction" 2008 [1], where it is introduced in the very interesting OO lecture. My plan is to learn some logic first though, specially relational logic, from Stanforfd's "Introduction to Logic" [2], which I am enjoying. There is also an Alloy book, with many examples like OO design and state machine based messaging protocols. [1] https://ocw.mit.edu/courses/electrical-engineering-and-computer-science/6-005-elements-of-software-construction-fall-2008 https://ocw.mit.edu/courses/electrical-engineering-and-compu... [2] http://intrologic.stanford.edu/lessons/lessons.html http://intrologic.stanford.edu/lessons/lessons.html