Specifying systems
Both a tutorial on specifying systems and a complete reference to TLA, this is the distillation of 25 years of work by a renowned computer scientist. Divided into four parts, the first part contains all that most programmers and engineers need to know about writing specifications. The second part has advanced material for more sophisticated readers. The third and fourth parts comprise a reference manual for TLA+--both the language itself as well as its tools.
Stats for nerds
18recommend
39mentions
24people
2015–2026years
64% recommend33% neutral3% critical
Mentions per year
What Hacker News says
- Mandatory Background:
1) Understanding Formal Methods by Jean-Francois Monin - This is the absolute best for getting a grip on the breadth, concepts and sample tools for Formal Mathematics/Specification/Verification. Fire-hose of information (not a step-by-step textbook) so use this as a map for everything "Formal". The S/N ratio is very high (~250 pages only!) so use AI/Textbooks to help explain concepts you find difficult to understand.
Practical:
1) Software Abstractions: Logic, Language, and Analysis by Daniel Jackson - Uses "Alloy" language to teach Structural (i.e. Data) Modeling.
2) Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers by Leslie Lamport - Uses "TLA+" language to teach Behavioural (i.e. State Machine) modeling.
The above two are for "System Modeling" i.e. everything needed to formally build complete systems.
3) Finally, You should also look at the bunch of free books on the Lean4 website which can be studied parallely for "code-level" proofs and verification.
PS: There are a few more (eg. Event-B method etc.) but you can get to those if/when you need to.
- I recently started reading "Specifying Systems: The TLA+ Language and Tools for Hardware and Software En" by Lawrence Lamport[0]. It is a good starting point for learning how to specify systems on the basis of mathematical proofs.
Since the new code is specifications in the age of AI, learning how to specify systems mathematically is a huge advantage because English is extremely ambiguous.
[0]: https://lamport.azurewebsites.net/tla/book-02-08-08.pdf
- Hillel Wayne wrote https://learntla.com/ which is quite good! Leslie Lamport also has a webpage of other possible learning resources, including a video course he put together where he wears many strange hats: https://lamport.azurewebsites.net/tla/learning.html
Personally I learned by reading the first few chapters of Specifying Systems.
- I found "Specifying Systems" by Lamport, and the examples it gives, to be an excellent introduction and a stricter companion to https://learntla.com.
It has some chapters that give very precise definitions of how things work in TLA (both on a language level as well as model checking), which answered some questions I often had along the way in more informal introductions.
- I think "Specifying Systems" by Leslie Lamport should be on the list.
Along with "Mastering Bitcoin: Programming the Open Blockchain Book" by Andreas Antonopoulos
- The book is probably "Specifying Systems" by Leslie Lamport[1].
I recently started reading this book and felt amazed at the way it progresses. It introduces Propositional logic, Predicate logic, and then Temporal logic. Enjoyed it so far and looking to apply it in the real-world.
Related
Software engineering mathematics
2 recommend · 4
2019–2026
Practical TLA+
15 recommend · 25
Compiler construction for digital computers
1 recommend · 7
Formal syntax and semantics of programming languages
2 recommend · 5
Structure and Interpretation of Computer Programs
347 recommend · 761
Matters computational
3 recommend · 11
