Comment by tombert
2 months ago
I am!
The author of FizzBee reached out to me about a year ago on LinkedIn actually, because I gave a talk on TLA+ a few years ago.
I haven't really played with it yet (outside of the few examples on their site) because I'm already pretty entrenched in the TLA+/PlusCal world, but it is very likely that FizzBee might be a better fit for software engineering circles; the incremental testing is pretty neat, to a point where I kind of want to steal the that and port it over to TLA+/TLC. Probabilistic testing seems pretty cool too.
If I were getting into Formal Methods today for the first time, I would almost certainly be using FizzBee and/or Alloy.
I have knowledge of FM primarily from HackerNews posts about it.
As someone lacking your academic background in it could you give me some advice on a good starting point, or perhaps papers/materials that are absolutely unskippable/foundational to understanding it, maybe a good learning exercise for utilizing FM?
FizzBee is likely a good place to start, but since I have never really used it I'm afraid I can't recommend good resources for it.
------
If you're just getting started, I recommend checking out my former advisor's book: https://www.amazon.com/Software-Engineering-Mathematics-Sei/...
I found this book to be fairly easy to read through, and gives you a rundown of a lot of the notation and concepts that pretty much all formal methods systems require.
------
TLA+ is a decent enough language. I recommend going through Lamport's video series on it to start: https://lamport.azurewebsites.net/tla/learning.html
I don't know what aspect of Formal Methods that you want to focus on; most of what I've done is with distributed systems stuff, but TLA+ can and has been used for low level things like circuit modeling. I can't tell you where to learn about that.
I think Hillel Wayne's learntla website is pretty good to get a few more practical examples: https://learntla.com/. I actually thought his Practical TLA+ book was a bit better for that though: https://www.amazon.com/Practical-TLA-Planning-Driven-Develop...
Both of those resources are more PlusCal focused. PlusCal is a C/Pascal-like language that compiles to "raw" TLA+. A lot of people like it more, I go back and forth.
If you care more about the more theoretical aspects of TLA+, Ron Pressler's "TLA+ in Practice and Theory" blog series is great: https://pron.github.io/tlaplus
Additionally, I recommend looking for the papers by Stefan Merz. Here's a good one to start, but he has a bunch: https://members.loria.fr/Stephan.Merz/papers/tla+logic.pdf
------
If your goal is to model concurrent systems, getting an understanding of CSP is worth doing. I liked Roscoe's book on it: https://link.springer.com/book/10.1007/978-1-84882-258-0
If you go deep into that, I recommend looking at the extension "tock-CSP" that adds timing semantics.
-------
If you're interested in the most theoretical aspects of formal methods, the only one I've done with any kind of intimate detail is Isabelle.
Isabelle is much more of a "math proof" thing than a "computer science" proof thing, but there are plenty of computer science things for it too. If you want to get started with the Isabelle/HOL language, the Concrete Semantics book is the normal recommended starting point: http://concrete-semantics.org/
------
This is mostly my history, there are many other paths but I can't really speak to those with any confidence. Hope this helped!
ETA:
Just to add, while I did go to school later for formal methods, I actually started learning this stuff while I was still a dropout from my undergrad. I eventually got my bachelors and masters and then entered a PhD program, but for TLA+ in particular I was learning it without any completed education, so this stuff is definitely approachable even without a ton of letters after your name.
Thank you so much for this quality reply!
I shared earlier in the thread about the learning app I'm working on. I already have a learning path created in it for Formal Methods. I will be taking each of your points and tracking my progress to completing them.
Just wanted you to know your effort won't be unappreciated.
1 reply →