A Computer Scientist Tells Mathematicians How to Write Proofs
blogs.scientificamerican.com
A Computer Scientist Tells Mathematicians How to Write Proofs
1–10 of 103 posts
Re: A Computer Scientist Tells Mathematicians How to Write Proofs
#2This could have been more precise. The example at the start was great, but there's no example of the lecturer's technique outside of the link to the actual lecture
Re: A Computer Scientist Tells Mathematicians How to Write Proofs
#3This could have been more precise. The example at the start was great, but there's no example of the lecturer's technique outside of the link to the actual lecture
There's a link to his paper:
http://research.microsoft.com/en-us/um/people/lamport/pubs/p...
Re: A Computer Scientist Tells Mathematicians How to Write Proofs
#4Basically, do it the way Spivak does. Funny thing is in freshman year we were taught to do just that, but then abandoned the formality pretty much immediately after.
Re: A Computer Scientist Tells Mathematicians How to Write Proofs
#5Could anyone with first-hand experience of TLA+ comment on how practical it actually is?
I've been toying with idea of trying this for a not-quite-trivial (programming!) project I'm working on, but the documentation and UX have so far kept me quite skeptical of using this "for real". The fact that I also can't turn the proof into a program in a semi-automated fashion also seems to indicate that there's at least some barrier where the "doubled" amount of work would be justified. (I'm more inclined towards something like Idris or LiquidHaskell which seem to support practical programming better and will probably let you get arbitrarily close to "proof" in any practical sense where proof will matter.)
I take it that this was mostly about mathematics and not implementations of programs, which may not quite have the same trade-offs. I still would like to hear from anyone with direct experience :).
Re: A Computer Scientist Tells Mathematicians How to Write Proofs
#6"I think most of us, including my math-phobic Facebook friends, would find the second version easier to follow and understand." I guess I'm in the minority. I preferred the words (though the translation was a bit ungainly).
Re: A Computer Scientist Tells Mathematicians How to Write Proofs
#7Basically, do it the way Spivak does. Funny thing is in freshman year we were taught to do just that, but then abandoned the formality pretty much immediately after.
My understanding from the linked paper in another thread, is not to do it the way Spivak does. That is, the article says Lamport "walked us through a proof of a corollary to the mean value theorem from that textbook, pointing out statements that he felt were not precise or rigorous enough and rewriting the proof using his technique."
My reading of that is that Lamport found faults in Spivak's approach. Did I missread that?
I will say that this really looks like a way to write proofs for computers to read, moreso than a way to write them for other people. Probably has great value, but not too surprising that it isn't widespread.
Re: A Computer Scientist Tells Mathematicians How to Write Proofs
#8Could anyone with first-hand experience of TLA+ comment on how practical it actually is? I've been toying with idea of trying this for a not-quite-trivial (programming!) project I'm working on, but the documentation and UX have so far kept me quite skeptical of using this "for real". The fact that I also can't turn the proof into a program in a semi-automated fashion also seems to indicate that there's at least some…
I was formerly in the same lab as Leslie. As a side project, we (Tom Rodeheffer, mainly) used TLA to verify the correctness of Naiad's coordination protocol. The protocol is very simple (distributed reference counting), and my initial "proof sketch" was about two paragraphs long (and very unconvincing, apparently :). Tom's TLA+ version was closing in on 200 pages, available at
http://research.microsoft.com/pubs/183826/paper.pdf
A short publication about it, with some reflective discussion of why it was hard to write down, is at
http://research.microsoft.com/pubs/199767/clock-verif2.pdf
My understanding is that part of the problem was that Tom needed to explain (re-prove) many meta-facts we take for granted.
Re: A Computer Scientist Tells Mathematicians How to Write Proofs
#9I just finished a course in Coq - it was pretty fun. Seems like something of the same the guys paper is about.
Re: A Computer Scientist Tells Mathematicians How to Write Proofs
#10Could anyone with first-hand experience of TLA+ comment on how practical it actually is? I've been toying with idea of trying this for a not-quite-trivial (programming!) project I'm working on, but the documentation and UX have so far kept me quite skeptical of using this "for real". The fact that I also can't turn the proof into a program in a semi-automated fashion also seems to indicate that there's at least some…
I've used it a bit for stuff inside Azure. It's difficult to find a problem where the model checker shines; state machines are far too simple (better to use P[1] or something similar), and something like cache coherence (the Hello World of real-world TLA+) isn't a problem I hit often.
TLA+ isn't only a model checker & theorem prover, though. The language itself is an excellent high-level way of expressing system design. Recently I've been applying it to eventually consistent systems, and writing an idea in TLA+ is a great way to flesh out the concept and spot hidden assumptions or edge cases. Lamport knows this; in the introduction to his TLA+ book, he quotes:
"Writing is nature's way of letting you know how sloppy your thinking is."
Followed by his own expansion on the concept:
"Our basic tool for writing specifications is mathematics. Mathematics is nature's way of letting you know how sloppy your writing is. ... The mathematics we use is more formal than the math you've grown up with. Formal mathematics is nature's way of letting you know how sloppy your mathematics is. The mathematics written by most mathematicians and scientists is not really precise. It's precise in the small, but imprecise in the large. Each equation is a precise assertion, but you have to read the accompanying words to understand how the equations relate to one another and exactly what the theorems mean. Logicians have developed ways of eliminating those words and making the mathematics completely formal and, hence, completely precise."
Most of the value I get from TLA+ is as a software design tool. It's also just a fun language to write stuff in.
You may also be interested in the AWS paper, which had excellent results.[2]
[1] https://plang.codeplex.com
[2] http://research.microsoft.com/en-us/um/people/lamport/tla/am...