4 ms·
As the author notes, Leslie Lamport makes much of the same point, but more rigorously. You can find it in many of his writings, e.g. http://lamport.azurewebsite
by pron 7y ago
As the author notes, Leslie Lamport makes much of the same point, but more rigorously. You can find it in many of his writings, e.g. http://lamport.azurewebsites.net/pubs/state-machine.pdf http://lamport.azurewebsites.net/pubs/state-machine.pdf
Lamport's TLA+ makes this formal. It is a language based on simple mathematics + some temporal logic for reasoning about discrete systems (software, hardware) as well as hybrid discrete-continuous systems, and is increasingly used in industy to lower the cost of software development (Amazon, Microsoft, Oracle and others). The idea of directly representing the relationships between abstractions and their implementation is the organizing principle of TLA+. For example, no program in any programming language (at least not in its runnable portion) can directly express Quicksort, as even though its specification (https://en.wikipedia.org/wiki/Quicksort https://en.wikipedia.org/wiki/Quicksort) is complete, none of its steps is deterministic enough to be conveyed to a computer; the best a programming language can do is describe one particular implementation (/realization/refinement) of Quicksort. In TLA+, you can specify Quicksort itself precisely, and then show that a particular sorting program is indeed an implementation of Quicksort.
- svieira 7y ago> and then show that a particular sorting program is indeed an implementation of Quicksort. I wasn't aware that TLA+ made this part possible. How do you map from TLA+ to C++ (for example) with certainty?
- pron 7y agoOh, you usually specify in multiple levels of detail in TLA+ and relate them and only informally relate them to code, but if you want a formal relation to code you could compile your program to TLA+ (e.g. http://tla2014.loria.fr/slides/methni.pdf http://tla2014.loria.fr/slides/methni.pdf). ... But you probably don't really want to do that. Code-level verification using any "deep specification" tool (TLA+, Coq, Isabelle, Lean, F* etc.) is extremely limited in scale compared to specifying in TLA+ at a higher level. Because there is no known way to directly verify programs larger than several thousand lines affordably, and because that's precisely the kinds of programs that most engineers need to verify most of the time, it's far more common to use TLA+ at a higher-than-code level.
- agentultra 7y agoRefinement calculus is what it's formally referred to as. As pr0n has mentioned you start with a high-level, abstract model. You then create a second model that implies every invariant of the first while adding more detail. You proceed like this to get closer to the implementation. If you are satisfied they are one and the same you can stop. However the goal isn't often to verify every single line of code. That would be prohibitively time consuming and expensive. The ideal use for this stuff is to verify the hard parts that are critical to get right. Verifying that a critical section of code will not lead to a deadlock or resource contention might be really important and so you could start with verifying that particular system.
- anaphor 7y agoFor most programs, you can just use PlusCal instead of straight TLA+ and get most of the benefits. Unless you're writing something that is heavily concurrent or distributed.
- pron 7y agoI prefer TLA+ (it's both simpler and more powerful than PlusCal), except when specifying something at the code level (e.g. something like weak-memory-model concurrency algorithm).
- hwayne 7y agoFor 95% of people, PlusCal will suit them just fine. I'm starting to see people say "I shouldn't learn PlusCal because it's not really TLA+", get disheartened about how difficult TLA+ is to learn, and believe they aren't able to use formal methods. I'd rather 10 people use a slightly-more-limited tool than 1 person use "the real thing".
- pron 7y agoI don't think TLA+ is "the real thing." I just find it easier. If others find PlusCal easier, then they should definitely start with that.
- raegis 7y agoI have the same opinion about the beauty of TLA+ vs PlusCal, so I find PlusCal frustrating to read. But I don't think the original poster was giving a dismissive opinion of PlusCal. Lamport's genius here is that he made TLA+ accessible via PlusCal. I appreciate this, as well as the video lectures which he made because he "realized that people don't read anymore...".
- anaphor 7y agoThe video lecture series is amazing and should be mandatory viewing for any CS or SE program IMO.