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):
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.
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.
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.
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?
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.
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.
This is essentially exactly what model checkers do. The big difference is that they exploit the structure of the problem description in order to reach exhaustiveness in “reasonable” time. This can be a big time saver over trying to do it manually.
I’d emphasize that using Alloy/TLA is often an iterative process where you refine your model over time. In this way, it’s possibly faster to dig through several iterations in Alloy before identifying a counter-example to a property of interest.
But if you are mostly interested in finding interesting test sets then you should be able to stop once you’ve modeled your actual implementation well enough.
Hmm. I don't use Alloy nor do I know hardware yet. I'll still try to dig up something. (comes back) It looks like a lot of CompSci folks built test generation in Alloy for languages such as Java. Might have not released any general tools for Alloy, though. Good news is they describe the benefits and some specifics where hardware people might get ideas for homebrew tools.
Honestly, I'd have thought TLA+ would be better of the two for hardware given it deals with concurrent things. Also, it can do stuff similar to SPIN model-checker that was used extensively for hardware verification in the past. For hardware, I'd have experimented with SPIN for lightweight method with ACL2 for heavyweight esp thanks to Jared Davis at Centaur contributing ACL2 components he used.
Just for kicks, I did some quick Googling on test generation for sequential circuits to see if I could find anything interesting for you. Me, too, as I enjoy seeing what people do in your field. Most were paywalled but this one wasn't:
Thanks for the links. My current application is not test generation for hardware, though. I'm working with autonomous robots that need to interact with real world obstacles that can't be easily predicted (laundary carts, golden retrievers, bride's maids....), need to navigate spaces where WiFi comes and goes, and need to interact with other automated systems running their own state machine that I don't control. Something that could identify "Recovery scenario needed here" has good value.
Apparently, I totally misread what you needed. Sorry. Your domain is very interesting. I briefly studied it a long time ago. They were using fusion of data coming from different components with quite non-deterministic algorithms such as fuzzy logic or neural networks. There wasn't any way to verify them at the time. I've seen a few attempts at such things but would need to know what kind of algorithm you use for sense, learn, and act (or whatever they call it). No guarantees here.
Alloy will tell you where things are over or under-specified. You can ask the system to generate you scenarios in the "world" so you can see a graphical representation of states. You can test/check your assumptions or operating criteria against the structures/rules of the of the "world" and it'll find and show you counter-examples where things fail. I especially like working in Alloy because it's incremental and interactive, like a REPL for you design work, providing some of the benefits of property-based testing in the design portions of creating your system. Simply put: It helps you think through and explore your design!
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.
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.
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).
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.
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.
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/
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.