Software abstractions

What Hacker News says

1. rramadassOct 2026
   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.

   Show morethread
2. l8againJun 2023
   If anyone is interested in learning more about Alloy, I would recommend this book by the author, Daniel Jackson - "Software Abstractions" - https://www.amazon.com/Software-Abstractions-Logic-Language-...
   thread
3. fspeechFeb 2019
   Alloy (and the philosophy it is based on) is explained in Daniel Jackson's book <<Software Abstractions>>, which is a very nice book to read on techniques of specification and verification (at the specification level).
   thread
4. fspeechMar 2015
   I bought Daniel Jackson's book Software Abstractions: Logic, Language and Analysis. It thoroughly discusses all aspects of Alloy software and methodology. I have to say it is one of the best software book I've ever read. It covers relational modelling thoroughly and is very readable from cover to cover. Model checking is so much more pleasant to use than theorem proving. The Alloy software download jar file also includes both source and examples.
   Show morethread
5. timClicksOct 2019
   I watched that earlier this week, and have been making my way through the Software Abstractions book by Jackson. Alloy's still in the "this thing makes me feel stupid" territory, but it does feel learn-able to me. I really like the emphasis on iterative development.
   thread