Disclosure: @jkoppel is a friend of mine and showed me the review before posting it. I’m reading people’s comments but not going to respond to anything- I don’t think it’s okay for authors to “intervene” in these kinds of discussions.
This was actually a decent review. Thorough, by someone who seems to know at least something about the field and can articulately express pros and cons. Worth a read if you’re interested in TLA+, or formal methods in general.
The only thing I’d push back on is the idea that Hillels book is the first “practical” book on formal methods, and I’d push back on that quite seriously. There are a number of books, going back years (decades?) that teach some aspect of what we now call “formal methods” that are eminently practical. The idea that because the examples given in the text are relate-able, “here’s a bank account model”, “this is some procedural code” or simply that its published by Apress is a little (forgive me!) parochial? Certified Programming with Dependent Types is an eminently practical book, you’re certifying common data structures one learns in school and that will absolutely show up anywhere a programmer is going to be doing the kind of work that necessitates formal methods. There are others along that line I could mention, but its worth pointing out the issue here in detail. If you’re going to be doing formal methods work, even just model checking as opposed to full on verification with a proof assistant, odds are strong that you’re not working on a CRUD app. While Hillel (and the review) point this out (the review nods at avionics), and clearly Hillel used it at a SaaS company for elearning, very, very few people are actually going to be able to get model checking approved by management as a stage of development. Amazon has become something of a non-defense/avionics poster child for this; not surprising given the scale of their systems and the money on the line and I think points to the stakes necessary for management to approve. I’d love, truly love to see formal methods more broadly adopted, I’m just not sure that the pedagogical tack necessary to successfully communicate the ideas and, er, methodology, is something that can be easily packaged as “practical” when so much of modern programming doesn’t yet or can’t be situated in a pure or semi-pure mathematical setting. The review itself kind of hints at this, by saying how the book by choosing to focus on PlusCal as opposed to pure TLA+ itself leads to a kind of obfuscation which hides the essential ideas.
Anyway, what I’ve read of the book is excellent, and this review gets to some of the issues of the text both positive and negative, when I have time to get back to the book I’ll absolutely have a tab open to this review to hopefully help guide me along if I get stuck somewhere.
Certified Programming with Dependent Types is an eminently practical book
That’s a good book I recommended to all kinds of people wanting to start on formal verification. Almost nobody took it up. Based on online comments, more people quit than finish on Software Foundations, too. That hints that these are not practical books for average programmer. They see a massive amount of work with minimal gain. Especially in a world where customers or FOSS users tolerate bugs which they patch eventually. Practical to these people has to provide significant benefits over what they’re doing with minimal investment. That’s why you see more uptake of fuzzing (esp AFL) and property-based testing. Low effort, high gain. They like static/dynamic analysis, too, if the tool is seemless with little to no false positives.
Note that safety-critical field isn’t any different. The people pushing code-level verification, static analyzers, and certifying compilers are doing hard sells. Frama-C and SPARK Ada have a tiny amount of industrial users. Astree Analyzer has some deployment like at Airbus. That field’s programmers mostly do careful coding in safer subsets, lots of review, and lots of testing. Like with regular developers, there seems to be more adoption of automated, test generators than formal methods. They wouldn’t care about CPDT either.
EDIT: While I was writing that, @brocooks came in with a comment showing exactly what I was talking about. The non-formal method was more familiar, easier to do, and got results. Probably likely to try something like that again in future before TLA+ or other formalism.
right, but the “non-formal method” is exactly what I, and the reviewer himself, were talking about in terms of hiding or obfuscating the ideas. If by practical you mean “people will read it” you’re not really saying much substantively, and you’re certainly not saying much in terms of the ideas within the texts themselves. You kind of side stepped right past that point in my (admittedly long) comment. I have high hopes for Hillels book, I like it! I just think that its not the first book to deserve the title of a practical introduction to formal methods. (Just for clarity, both to Hillel and anyone else reading this, I’m referring to the line in the review about being a “practical introduction to formal methods”, the practical in the title of the book is fine, given that that is exactly what it is, a practical intro to TLA+)
“ If by practical you mean “people will read it” “
I mean something the majority of developers… using C#/Java/Javascript/PHP/Python… might read, see some value in it, and maybe apply it to some degree. Most formal methods books, including Chlipala’s, don’t meet that minimum requirement. They will certainly get ignored. Wait, why talk future tense: they were and are being ignored by most developers. Which is fine if they’re aimed at a different, smaller audience. This one wants to appeal to the huge swath of programmers ignoring all the books on formal verification, type theory, etc. Their definition of practical is different than an aspiring language theorist or proof engineer that might benefit from works like Chlipala and Pierce.
“I just think that its not the first book to deserve the title of a practical introduction to formal methods.”
I agree with that. To me it’s a recent, practical intro. The first ones might have been something for Z or VDM which had some use in industry. Maybe SRI’s stuff or Gypsy if they had any educational books. I haven’t looked in a long time.
I don’t think formal methods is going to be used by “the majority of developers”, whatever that aggregate actually means, because the kind of work that they do isn’t going to be helped by formal methods. You also still haven’t responded to the point about what an appropriate pedagogy looks like, because to actually make use of model checking you’re going to need to understand some serious logic, and if the road to getting people to read your book involves jettisoning that material then you haven’t really helped the reader! I don’t think Practical TLA+ outright does that, in fact I think that the choices he made were by and large the right ones, but I also don’t think you can adequately claim to have “practically” brought formal methods to the masses if you side step the “formal” part. Chlipalas book(s) are perfectly approachable, I don’t blame him or the books for them going unread, I blame a programming culture that hisses and wails and gnashes its teeth at things like rust, because g-d forbid we attempt to move beyond C/C++. I blame all of the old hands who sneer at formal methods because model checkers didn’t get fast until the last decade. I also blame a technical community that scorns academic research for any of a number of reasons, not the least of which is that a sizeable portion of the workforce is more or less self taught.
This was a nice review. I admit I wasn’t able to finish the book, as I constantly got stuck on the confusing PlusCal syntax.
At the time of reading it, I was getting some weird edge cases in a distributed protocol at work, and trying to come up with a minimal example that could be reproduced was proving to be quite difficult. I got the book after reading a couple of Hillel’s posts and seeing the announcement here, with the idea of using TLA+ to solve our issue.
I already had a written specification (although in pseudocode form, and quite loose), and some intuition of where the problem was coming from, so I thought it would be a simple task. Nevertheless, I was never able to do it. Trying to reduce the real implementation to a model that TLA could understand, and figuring out the right level of detail, proved to be too time consuming, plus I had other, more urgent things to do, and in any case the problem was rare enough to be able to postpone finding a solution for a bit.
Fast forward a couple of months, and I finally decided to come back to the problem. This time, though, I implemented a simplified version of the system, in real code, and ran it through a property-based test (poor man’s model checker) that would execute actions against the system, and specified that the edge case would never happen. I didn’t get the prettiest execution on the first try, but I managed to refine it iteratively and armed with existing knowledge of the domain. The final execution was maybe 10 lines long as easily explainable in a whiteboard, which I consider a great success.
The whole thing took maybe a week of work (counting reading about model-checking, property tests and learning to use the testing library) and proved much simpler than trying to tackle a real TLA spec. I’m not saying my approach was better, TLA can express so much in terms of temporal properties that trying to model that some other way will be painful. But sometimes, the simplest approach works best.
I’ve also had a lot of success using property-based testing as a sort of model checker, but there are trade-offs to keep in mind. I’ve been learning TLA+, off and on, and don’t feel it’s at all redundant with property-based testing.
TLA+ will check the model exhaustively, whereas every property testing library I’m aware of is probabilistic – because they’re semi-randomly exploring, it’s never certain when they’ve checked all meaningful cases, and some are better than others about avoiding redundant checks. Sometimes the partiality is fine, and just random stress testing is a good way to feel out an implementation, but total state-space coverage is compelling.
Where TLA+ checks a model of the code, a property testing library will check the implementation (or perhaps a subset). It’s often worth doing both! I mostly work in C these days (and use my theft library for property-based testing), so testing for mistakes in the implementation details is pretty important, but a non-code model checker could still be really valuable during system design.
TLA+ will check the model exhaustively, whereas every property testing library I’m aware of is probabilistic.
For sure! A naïve property might not find the example you’re looking for. I know I didn’t get anything on my first try. I had to play a lot with the model generator and the shrinking procedure, to the point that I ended up defining explicitly certain parameters of the generator (number of concurrent processes, number of operations a process is able to execute, etc).
It’s often worth doing both!
Won’t disagree here, if I had already known TLA or any other specification language, I would’ve use that for sure (and if I ever get the time I plan to come back to the book and work through it, plus Lamport’s book), but when you’re facing constraints in the available time you have, going for a simpler solution can get you far enough.
That seems like a fair review. I had a look at both Practical TLA+ and Lamport’s book after seeing a video where Hillel convinced me these were useful things, and decided that I’d rather learn TLA+ than a language that compiled to it. Admittedly, I was a mathematician in a former life and am comfortable with set-based ideas and notations. The examples in Hillel’s book are very nice; one day I’d like to really sit down to learn TLA+ by implementing those examples in it rather than in PlusCal.
I hate the typesetting in this book, and I was initially disappointed by its scope, but it’s a great book, most importantly because it’s something I can hand to someone whose eyes would glaze over with any of the usual literature on formal methods, which is a huge win in convincing a team to adopt them.
re refinement. I’m not sure how appropriate that is given Hillel’s audience. This goes back to what is meant by practical, which is tripping @dtornabene up. He’s targeting programmers who aren’t going to learn formal verification, have no math background, need stuff familiar, and will be lured in by quick, easy results on realistic problems. So, instead of code-level verification, he pushes them mocking their designs up in ways that will catch problems other methods won’t.
He does have a series of articles on another lightweight method, Design by Contract, to help them on the implementation. Maybe he’ll link them in future like this work (pdf) does. Regardless, they have to get something in return they can’t get with push-button tools like AFL. So far, most haven’t even been interested in using formal specs w/ automated solvers in SPARK Ada prove absence of errors they debug regularly. What low-effort, high-gain lessons on refinement would you suggest for such a tough crowd?
re deep errors. I’m glad you linked the Amazon example. We all need to keep collecting examples of such deep or corner bugs that testing can’t find or rarely finds. Especially that drain a ridiculous amount of time to find and fix after deployment. Eliminating them is one of highest returns of these tools. Plus, a developer would have to lie to themselves to believe they’d find the one with 35 steps. We need to repeat that number till we’re blue in the face. ;)
re syntax. Glad you brought that up. Better syntax might help in adoption given how finicky developers are about syntax. Maybe a few front-ends for people of different backgrounds. One thing you said, where things executed in parallel, was addressed in parallel languages by putting “par” before the statement’s normal name. So, for is sequental, parfor is parallel. Might work in future syntax.
re temporal logic. This might be legitimate gripe. I’m not sure. The book appears to aim for breadth instead of depth to cast wide net. The examples, from data structures to CRUD-like apps, make me think that. It also needs immediate value with lazy/busy non-mathematicians. He covers basic concurrency, multiple readers/writers, ordering, deadlocks, termination, and stuttering/liveliness. That’s almost all the concurrency errors regular developers talk about. Maybe I’m overlooking one since I’m still drinking coffee. Off top of head, it looks like he looked back on what they griped about the most, made a lesson for each one, and then left rest of temporal logic as a lure for them to hit heavier resources if interested enough. Most won’t be. Those might even be scared off if he unloaded two, hard topics (TL and TLA+) on them at once.
https://lamport.azurewebsites.net/tla/practical-tla.html?back-link=learning.html is what Lamport has to say about “Practical TLA+”.
Thanks, this inspired me to start learning TLA+ (in addition to my previous PlusCal experience) from Lamport’s video series!
(It includes PDF script/slides.)
Disclosure: @jkoppel is a friend of mine and showed me the review before posting it. I’m reading people’s comments but not going to respond to anything- I don’t think it’s okay for authors to “intervene” in these kinds of discussions.
This was actually a decent review. Thorough, by someone who seems to know at least something about the field and can articulately express pros and cons. Worth a read if you’re interested in TLA+, or formal methods in general.
The only thing I’d push back on is the idea that Hillels book is the first “practical” book on formal methods, and I’d push back on that quite seriously. There are a number of books, going back years (decades?) that teach some aspect of what we now call “formal methods” that are eminently practical. The idea that because the examples given in the text are relate-able, “here’s a bank account model”, “this is some procedural code” or simply that its published by Apress is a little (forgive me!) parochial? Certified Programming with Dependent Types is an eminently practical book, you’re certifying common data structures one learns in school and that will absolutely show up anywhere a programmer is going to be doing the kind of work that necessitates formal methods. There are others along that line I could mention, but its worth pointing out the issue here in detail. If you’re going to be doing formal methods work, even just model checking as opposed to full on verification with a proof assistant, odds are strong that you’re not working on a CRUD app. While Hillel (and the review) point this out (the review nods at avionics), and clearly Hillel used it at a SaaS company for elearning, very, very few people are actually going to be able to get model checking approved by management as a stage of development. Amazon has become something of a non-defense/avionics poster child for this; not surprising given the scale of their systems and the money on the line and I think points to the stakes necessary for management to approve. I’d love, truly love to see formal methods more broadly adopted, I’m just not sure that the pedagogical tack necessary to successfully communicate the ideas and, er, methodology, is something that can be easily packaged as “practical” when so much of modern programming doesn’t yet or can’t be situated in a pure or semi-pure mathematical setting. The review itself kind of hints at this, by saying how the book by choosing to focus on PlusCal as opposed to pure TLA+ itself leads to a kind of obfuscation which hides the essential ideas.
Anyway, what I’ve read of the book is excellent, and this review gets to some of the issues of the text both positive and negative, when I have time to get back to the book I’ll absolutely have a tab open to this review to hopefully help guide me along if I get stuck somewhere.
That’s a good book I recommended to all kinds of people wanting to start on formal verification. Almost nobody took it up. Based on online comments, more people quit than finish on Software Foundations, too. That hints that these are not practical books for average programmer. They see a massive amount of work with minimal gain. Especially in a world where customers or FOSS users tolerate bugs which they patch eventually. Practical to these people has to provide significant benefits over what they’re doing with minimal investment. That’s why you see more uptake of fuzzing (esp AFL) and property-based testing. Low effort, high gain. They like static/dynamic analysis, too, if the tool is seemless with little to no false positives.
Note that safety-critical field isn’t any different. The people pushing code-level verification, static analyzers, and certifying compilers are doing hard sells. Frama-C and SPARK Ada have a tiny amount of industrial users. Astree Analyzer has some deployment like at Airbus. That field’s programmers mostly do careful coding in safer subsets, lots of review, and lots of testing. Like with regular developers, there seems to be more adoption of automated, test generators than formal methods. They wouldn’t care about CPDT either.
EDIT: While I was writing that, @brocooks came in with a comment showing exactly what I was talking about. The non-formal method was more familiar, easier to do, and got results. Probably likely to try something like that again in future before TLA+ or other formalism.
right, but the “non-formal method” is exactly what I, and the reviewer himself, were talking about in terms of hiding or obfuscating the ideas. If by practical you mean “people will read it” you’re not really saying much substantively, and you’re certainly not saying much in terms of the ideas within the texts themselves. You kind of side stepped right past that point in my (admittedly long) comment. I have high hopes for Hillels book, I like it! I just think that its not the first book to deserve the title of a practical introduction to formal methods. (Just for clarity, both to Hillel and anyone else reading this, I’m referring to the line in the review about being a “practical introduction to formal methods”, the practical in the title of the book is fine, given that that is exactly what it is, a practical intro to TLA+)
“ If by practical you mean “people will read it” “
I mean something the majority of developers… using C#/Java/Javascript/PHP/Python… might read, see some value in it, and maybe apply it to some degree. Most formal methods books, including Chlipala’s, don’t meet that minimum requirement. They will certainly get ignored. Wait, why talk future tense: they were and are being ignored by most developers. Which is fine if they’re aimed at a different, smaller audience. This one wants to appeal to the huge swath of programmers ignoring all the books on formal verification, type theory, etc. Their definition of practical is different than an aspiring language theorist or proof engineer that might benefit from works like Chlipala and Pierce.
“I just think that its not the first book to deserve the title of a practical introduction to formal methods.”
I agree with that. To me it’s a recent, practical intro. The first ones might have been something for Z or VDM which had some use in industry. Maybe SRI’s stuff or Gypsy if they had any educational books. I haven’t looked in a long time.
I don’t think formal methods is going to be used by “the majority of developers”, whatever that aggregate actually means, because the kind of work that they do isn’t going to be helped by formal methods. You also still haven’t responded to the point about what an appropriate pedagogy looks like, because to actually make use of model checking you’re going to need to understand some serious logic, and if the road to getting people to read your book involves jettisoning that material then you haven’t really helped the reader! I don’t think Practical TLA+ outright does that, in fact I think that the choices he made were by and large the right ones, but I also don’t think you can adequately claim to have “practically” brought formal methods to the masses if you side step the “formal” part. Chlipalas book(s) are perfectly approachable, I don’t blame him or the books for them going unread, I blame a programming culture that hisses and wails and gnashes its teeth at things like rust, because g-d forbid we attempt to move beyond C/C++. I blame all of the old hands who sneer at formal methods because model checkers didn’t get fast until the last decade. I also blame a technical community that scorns academic research for any of a number of reasons, not the least of which is that a sizeable portion of the workforce is more or less self taught.
This was a nice review. I admit I wasn’t able to finish the book, as I constantly got stuck on the confusing PlusCal syntax.
At the time of reading it, I was getting some weird edge cases in a distributed protocol at work, and trying to come up with a minimal example that could be reproduced was proving to be quite difficult. I got the book after reading a couple of Hillel’s posts and seeing the announcement here, with the idea of using TLA+ to solve our issue.
I already had a written specification (although in pseudocode form, and quite loose), and some intuition of where the problem was coming from, so I thought it would be a simple task. Nevertheless, I was never able to do it. Trying to reduce the real implementation to a model that TLA could understand, and figuring out the right level of detail, proved to be too time consuming, plus I had other, more urgent things to do, and in any case the problem was rare enough to be able to postpone finding a solution for a bit.
Fast forward a couple of months, and I finally decided to come back to the problem. This time, though, I implemented a simplified version of the system, in real code, and ran it through a property-based test (poor man’s model checker) that would execute actions against the system, and specified that the edge case would never happen. I didn’t get the prettiest execution on the first try, but I managed to refine it iteratively and armed with existing knowledge of the domain. The final execution was maybe 10 lines long as easily explainable in a whiteboard, which I consider a great success.
The whole thing took maybe a week of work (counting reading about model-checking, property tests and learning to use the testing library) and proved much simpler than trying to tackle a real TLA spec. I’m not saying my approach was better, TLA can express so much in terms of temporal properties that trying to model that some other way will be painful. But sometimes, the simplest approach works best.
I’ve also had a lot of success using property-based testing as a sort of model checker, but there are trade-offs to keep in mind. I’ve been learning TLA+, off and on, and don’t feel it’s at all redundant with property-based testing.
TLA+ will check the model exhaustively, whereas every property testing library I’m aware of is probabilistic – because they’re semi-randomly exploring, it’s never certain when they’ve checked all meaningful cases, and some are better than others about avoiding redundant checks. Sometimes the partiality is fine, and just random stress testing is a good way to feel out an implementation, but total state-space coverage is compelling.
Where TLA+ checks a model of the code, a property testing library will check the implementation (or perhaps a subset). It’s often worth doing both! I mostly work in C these days (and use my theft library for property-based testing), so testing for mistakes in the implementation details is pretty important, but a non-code model checker could still be really valuable during system design.
For sure! A naïve property might not find the example you’re looking for. I know I didn’t get anything on my first try. I had to play a lot with the model generator and the shrinking procedure, to the point that I ended up defining explicitly certain parameters of the generator (number of concurrent processes, number of operations a process is able to execute, etc).
Won’t disagree here, if I had already known TLA or any other specification language, I would’ve use that for sure (and if I ever get the time I plan to come back to the book and work through it, plus Lamport’s book), but when you’re facing constraints in the available time you have, going for a simpler solution can get you far enough.
That seems like a fair review. I had a look at both Practical TLA+ and Lamport’s book after seeing a video where Hillel convinced me these were useful things, and decided that I’d rather learn TLA+ than a language that compiled to it. Admittedly, I was a mathematician in a former life and am comfortable with set-based ideas and notations. The examples in Hillel’s book are very nice; one day I’d like to really sit down to learn TLA+ by implementing those examples in it rather than in PlusCal.
I hate the typesetting in this book, and I was initially disappointed by its scope, but it’s a great book, most importantly because it’s something I can hand to someone whose eyes would glaze over with any of the usual literature on formal methods, which is a huge win in convincing a team to adopt them.
re refinement. I’m not sure how appropriate that is given Hillel’s audience. This goes back to what is meant by practical, which is tripping @dtornabene up. He’s targeting programmers who aren’t going to learn formal verification, have no math background, need stuff familiar, and will be lured in by quick, easy results on realistic problems. So, instead of code-level verification, he pushes them mocking their designs up in ways that will catch problems other methods won’t.
He does have a series of articles on another lightweight method, Design by Contract, to help them on the implementation. Maybe he’ll link them in future like this work (pdf) does. Regardless, they have to get something in return they can’t get with push-button tools like AFL. So far, most haven’t even been interested in using formal specs w/ automated solvers in SPARK Ada prove absence of errors they debug regularly. What low-effort, high-gain lessons on refinement would you suggest for such a tough crowd?
re deep errors. I’m glad you linked the Amazon example. We all need to keep collecting examples of such deep or corner bugs that testing can’t find or rarely finds. Especially that drain a ridiculous amount of time to find and fix after deployment. Eliminating them is one of highest returns of these tools. Plus, a developer would have to lie to themselves to believe they’d find the one with 35 steps. We need to repeat that number till we’re blue in the face. ;)
re syntax. Glad you brought that up. Better syntax might help in adoption given how finicky developers are about syntax. Maybe a few front-ends for people of different backgrounds. One thing you said, where things executed in parallel, was addressed in parallel languages by putting “par” before the statement’s normal name. So, for is sequental, parfor is parallel. Might work in future syntax.
re temporal logic. This might be legitimate gripe. I’m not sure. The book appears to aim for breadth instead of depth to cast wide net. The examples, from data structures to CRUD-like apps, make me think that. It also needs immediate value with lazy/busy non-mathematicians. He covers basic concurrency, multiple readers/writers, ordering, deadlocks, termination, and stuttering/liveliness. That’s almost all the concurrency errors regular developers talk about. Maybe I’m overlooking one since I’m still drinking coffee. Off top of head, it looks like he looked back on what they griped about the most, made a lesson for each one, and then left rest of temporal logic as a lure for them to hit heavier resources if interested enough. Most won’t be. Those might even be scared off if he unloaded two, hard topics (TL and TLA+) on them at once.