TLA+ in one sentence: it is a language used to write specifications, same as you might write a spec in English/your chosen informal language, except here you write your spec in basic mathematics; benefits of a formal specification language include freedom from ambiguity, model-checking, and even machine-checked proofs of correctness.
This language is a joy to use and I've found it really affects the way I think about system design.
It feels almost like an intentional joke. Do you think that is the case? Or just even short segments were recorded on different days and Lamport like to wear all sorts of hats? That one where he's wearing a beanie and indoor sunglasses seems particularly intentional.
I've never met him, and the delivery of the lecture seems fairly dry and serious, so I can't tell :)
Do you know of any straight forward non-trivial examples? Something a little more complex than "hello world" and something that isn't abstract?
The Wikipedia article also has some good example specs[3].
For your own first specification, I personally cut my teeth on a river-crossing puzzle with a farmer, wolf, and sheep.
[0] https://github.com/tlaplus/Examples/tree/master/specificatio...
[1] https://www.youtube.com/watch?v=6cAbgAaEOVE
[2] https://github.com/tlaplus/Examples/blob/master/specificatio...
If you're interested in learning more, I also wrote a beginner's guide[1] to the language, which contains concrete examples and exercises.
[0] https://medium.com/espark-engineering-blog/formal-methods-in...
SAM can also be used for stateful API/Microservice orchestrations [2]
If you want a slightly more formal introduction to SAM and its relationship to TLA+ (again, based on my own interpretation) I gave this lecture last month [3].
[2] http://www.ebpml.org/blog15/2015/06/designing-a-reliable-api...
[3] http://cloudsentinel.com/sam-state-machines-and-computation....
I think it would help to have a good mentor, as I did, or a lecture series from the language inventor. I ran through the trial version of these videos when Lamport was developing them and it's quite approachable even for someone who's more of a liberal arts kind of person.
There might come a day where TLAPS is as powerful as Coq for writing general mathematical proofs (indeed, better ways of writing proofs and mathematics seem to be a passion of Dr. Lamport's, see his paper How to Write a 21st Century Proof[0]), but for now it's far, far easier to prove even simple statements about the Natural numbers in Coq.
1. Difference in theory -- the theory of computation in Coq and HOL is based on functional programming; especially in Coq (I know very little about HOL), algorithms are functions in the FP sense (lambda expressions). In TLA, algorithms are state machines, and there's a richer notion of relationship between algorithms. This makes some things easier in TLA: Instead of programs being equal extensionally or definitionally, they can be equal or similar in many ways. In fact, in TLA there's a partial order relation on algorithms that reflects the refinement/abstraction relation. Also, it means that different kinds of algorithms -- sequential, concurrent, parallel, realtime etc., are all defined in the same way using the exact same ideas. This also makes it very easy to specify some properties -- such as worst-case complexity -- that are tricky in Coq. Having said that, people working on realtime systems in Coq implemented a simple version of TLA in Coq.
2. Differences in goals and audience -- Coq and HOL are ultimately general mathematical proof assistants. TLA+ is a tool for reasoning about digital systems. Coq and HOL can obviously reason about programs and TLA+ can prove general math theorems, but the focus is different. For example, Coq is used by logicians to explore new logics and mathematical foundations; you don't want to use TLA+ for that. On the other hand, TLA+ is used by "ordinary" engineers in industry working on "ordinary" software, while Coq and HOL are virtually unused in industry, and in the few cases they are, it's almost always in conjunction with academics and academic projects.
3. Differences in tools/abilities -- Coq can generate runnable code and be used for end-to-end verification. TLA+ cannot generate code, and while it has been used by academics for end-to-end verification, that is most certainly not its intended use. It is intended to be used in modeling large, complex systems at an abstraction level that's significantly higher than the code to find errors in design. As far as general math proofs are concerned, Coq is more capable than TLAPS, the TLA+ proof system. On the other hand, TLA+ has a model-checker that makes its proof checker almost irrelevant for large, complex specifications. As the users of TLA+ usually don't require a 100% watertight end-to-end specification, they're content to get the less than 100% guarantee of the model checker in exchange for what is at least a one order of magnitude reduction in effort.
In short, I would say that tools like Coq have a more academic focus, and are in general more interesting to academics and less to engineers, while TLA+ has a more industrial focus, and is of more interest to engineers and less to academics.
But I will repeat and say that while there are big difference in theory, goals and usage, ultimately when working on verifying software, the challenge is in thinking about your system mathematically and understanding how and why it works (or not). This work is similar both in effort and technique no matter what formalism you choose to use.
I've only ever heard of it's use in the formalization of distributed systems.
1. Lamport's algorithmic work is in concurrent and distributed algorithms, and as he uses TLA for his own algorithms -- and he's TLA+'s first user -- that's how it's known.
2. Few other general software verification formalisms are able to handle concurrency as easily as TLA, so that is where it shines in comparison. Of course, this is intentional because Lamport designed TLA+ to work well for the kinds of algorithms he's interested in.
3. When engineers write software systems that are too complex or subtle to be obviously correct, and could therefore benefit from formal verification, it is usually the case that a concurrent or distributed algorithm is involved.
Having said that, there is nothing specific about TLA+ that makes it any less suitable for sequential algorithms. If you write one that you think is complicated or subtle enough to require help in reasoning, you could certainly benefit from TLA+.
But if you're interested just in sequential algorithms, you do have more options, like Why3/WhyML, which I think is very nice (although I prefer TLA+). Whether WhyML or TLA+ would be better suited to verify your sequential algorithm depends largely on personal aesthetic preferences, as well as some details of requirements. For example, WhyML can generate OCaml code, while TLA+ can't. On the other hand, TLA+ has both SMT solvers and a model checker, which makes it more likely that you can verify the entire algorithm automatically, while WhyML requires manual proof in Isabelle or Coq for properties the automatic solvers can't verify (I hear they're working on a proof language directly in Why; I hope it's as nice as TLA+'s proof language). Also, TLA+ lets you describe your algorithm at various levels of abstraction, and show that the more detailed ones implement the more abstract ones. WhyML is more focused on the abstraction level of actual program code.
I do QA work and for quite some time I have been intrigued by property based testing. But we are usually testing lot of interconnected micro-services and when I tried to define test-scenario in i.e. quick-check, the end-result was always too complicated to maintain.
I basically tried to do a similar thing to John Hughes "Mysteries of Dropbox" paper.
It seems that with temporal logic it would have been much easier to specify the expected behavior of the program and then use the generated trace to instrument the live service and check that all of the properties still hold.
I'd love to see you implement this and write about your experiences.
So you can't guarantee your implementation matches your spec. All the more reason to write unit tests!
Didn't use it, but watch a few presentations, i.e: https://channel9.msdn.com/Events/Lang-NEXT/Lang-NEXT-2012/Bl...
C: http://link.springer.com/chapter/10.1007/978-3-319-17581-2_1...
Java: http://ieeexplore.ieee.org/document/6042069
The C work seems more thorough.
"What kind of clown am I claiming that I know what can make you think better? ... This is not the time to be modest. I have done seminal research in the theory of distributed and concurrent systems for which i won the turning award. You can stop the video now and look me up on the web. <long pause>..."
Achievement of the highest professional accolade for the very stuff that he plans to discuss is literally prima facie evidence in support of that claim.
I won't even try to use TLA+ in my business context. Just will search for a good java library. Maybe these videos will help me to recognize a good one?
BTW, do any of my HN's fellows have a good Java state machine opens source library to recommend?
[1] http://akka.io [2] http://erlang.org/documentation/doc/4.8.2/doc/design_princip... [3] http://doc.akka.io/docs/akka/current/java/fsm.html
Readable (kind of) here: https://www.yumpu.com/en/document/view/40763566/a-formal-des...
But there's been more recent work done in TLA+ on another realtime OS, where the mechanical proof system, TLAPS, was used to prove some aspects of the kernel correct, and you can read about it for free here: https://members.loria.fr/SMerz/papers/abz2016-pharos.html
(To understand PlusCal, you need first understand the basics of TLA+, but you don't need to understand the action system 100% in-depth.)
The idea behind PlusCal is to write your algorithm in it, leaving out the "unimportant" bits, and using the nondeterministic operators in place of any value that is not in your algorithm's control. The model checker, TLC, can then run all possible traces of your algorithm to search for conditions under which it may deadlock or violate some assertion you have made.
from wikipedia
What do people think of the format? I have off and on been thinking about a format where the video is the main highlight, but is supported, like this one, with links and other media to make it a more engaging experience. Are there other use cases that you think this would be conducive for?
*edit: sorry I see the link after the end of video#1...
