4 ms·

I'm surprised they didn't mention Leslie Lamport. He apparently started writing "structured proofs" decades ago, and then developed a system TLA+ to do the sam

by chubot 12y ago

I'm surprised they didn't mention Leslie Lamport. He apparently started writing "structured proofs" decades ago, and then developed a system TLA+ to do the same thing in a computer. I am hazy on the details, but I think TLA+ proofs are just checked by brute force, and not with an actual theorem prover? It's for distributed algorithms with a large but finite number of states. So it's not exactly the same as what's discussed in the article, but it's definitely related. I would appreciate if anyone has any clarification on this point. https://scholar.google.com/scholar?cluster=14553320809011812377&hl=en&as_sdt=0,5&sciodt=0,5 https://scholar.google.com/scholar?cluster=14553320809011812... "A method of writing proofs is described that makes it harder to prove things that are not true. The method, based on hierarchical structuring, is simple and practical. The author's twenty years of experience writing such proofs is discussed." http://research.microsoft.com/en-us/um/people/lamport/pubs/pubs.html#wired http://research.microsoft.com/en-us/um/people/lamport/pubs/p...

nmrm2 12y 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 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+.)

by chubot 12y ago

nmrm2 12y 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 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+.)