2 ms·
TLA+ is better described as a verification tool than as a proof assistant, and is better suited to analysis of software systems than to analysis of the sort of
by nmrm2 11y ago
TLA+ is better described as a verification tool than as a proof assistant, and is better suited to analysis of software systems than to analysis of the sort of mathematics in which Voevodsky is involved. The most striking characteristics that make Coq and other tools based on dependent type theories interesting to Voevodsky are absent from systems like TLA+.
TLA+ is sufficiently different from Coq -- and in ways essential to Voevodsky's intentions -- that discussion of TLA+ in this article would be out of place.
In addition, there is a huge community of people who have worked with theorem provers for the past 20 years or more; it's not clear to me why the author would single out TLA+/Lamport over any of these other systems/researchers.
- chubot 11y agoSure, but the motivation is the same: to avoid proving things that aren't true. Lamport and Voevodsky are in different fields, and use different tools, but that just means that comparing their journeys is all the more interesting. If it were a technical journal, maybe they wouldn't be related. But they're definitely related for a popular article.
- nmrm2 11y ago> If it were a technical journal, maybe they wouldn't be related. But they're definitely related for a popular article. Hence my last paragraph -- they're only related in the sense that the entire formal methods/verification/theorem proving community is related. Given the hundreds of systems/researchers that would make for interesting additions to the story, it's not surprising that TLA+ isn't mentioned. (Incidentally, the author's choice representative for "other people are doing this too" -- Automath -- is probably just as good of a choice as TLA+.)