3 ms·
Sure, 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 tha
by chubot 12y ago
Sure, 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 12y 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+.)