6 ms·

Software Foundations

138 points by rfreytag 9y ago

rambojazz 9y ago
Do these books come with a free license?
- dtornabene 9y ago
  click through, they're in html
  - dqpb 9y ago
    Ironically, they are rather hard to click through. You have to return to the toc to get to each next chapter.
- yorwba 9y ago
  They are MIT-licensed. (At least the archive for Logical Foundations is.)
lou1306 9y ago
This is really neat, but in my opinion conflating theory and actual verification through Coq might be a bit too much for a newcomer. For those who are looking for a softer introduction to the field, I highly recommend "Reactive Systems: Modelling, Specification and Verification" by Aceto, Ingólfsdóttir, Larsen, and Srba (full disclosure, I am a student at Aceto's current affiliation).
nickpsecurity 9y ago
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
auggierose 9y ago
These are very pretty books, and at the same time very ugly. Thank god I already know the material in these books, I wouldn't want to learn it this way.
ahelwer 9y ago
These are the perfect books to work through on a Sunday afternoon. Did the first part of Logical Foundations three years ago, and still look back on that day with fondness. Nothing has scratched that itch for perfect machine-enforced certainty in quite the same way since then.

138 points by rfreytag 9y ago

rambojazz 9y ago

Do these books come with a free license?

dtornabene 9y ago
click through, they're in html
- dqpb 9y ago
  Ironically, they are rather hard to click through. You have to return to the toc to get to each next chapter.
yorwba 9y ago
They are MIT-licensed. (At least the archive for Logical Foundations is.)

lou1306 9y ago

This is really neat, but in my opinion conflating theory and actual verification through Coq might be a bit too much for a newcomer. For those who are looking for a softer introduction to the field, I highly recommend "Reactive Systems: Modelling, Specification and Verification" by Aceto, Ingólfsdóttir, Larsen, and Srba (full disclosure, I am a student at Aceto's current affiliation).

nickpsecurity 9y ago

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

auggierose 9y ago

These are very pretty books, and at the same time very ugly. Thank god I already know the material in these books, I wouldn't want to learn it this way.

ahelwer 9y ago

These are the perfect books to work through on a Sunday afternoon. Did the first part of Logical Foundations three years ago, and still look back on that day with fondness. Nothing has scratched that itch for perfect machine-enforced certainty in quite the same way since then.