A Computer Scientist Tells Mathematicians How to Write Proofs • Hacker News Board

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#11

Post by toolslive » Thu, Jan 29, 2015, 7:04 PM UTC

frankmcsherry wrote: post #8

lomnakkus wrote: post #5

Could 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/18382…

for distributed protocols, you might want to try Alloy. Basically it allows you to find counter examples (which are in this case scenarios). http://www2.research.att.com/~pamela/zave_podc.pdf is a well known example, working on the Chord join/leave protocol.

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#12

Post by ekarulf » Thu, Jan 29, 2015, 7:07 PM UTC

madsravn wrote: post #9

I just finished a course in Coq - it was pretty fun. Seems like something of the same the guys paper is about.

My discrete math and logic undergraduate course was in Coq. It was a brutal way to learn the proof process at first but it was worth the investment by the end. It's the logic equivalent of TDD.

If you are interested in computational logic you might enjoy Aaron Stump from UIowa's work: https://queuea9.wordpress.com/

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#13

Post by orbitur » Thu, Jan 29, 2015, 7:08 PM UTC

NSMeta wrote: post #3

thejaredhooper wrote: post #2

This 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...

Right. It would have been nice to have a short yet more in-depth example in the article.

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#14

Post by tormeh » Thu, Jan 29, 2015, 7:13 PM UTC

The problem isn't notation in itself; it's rarely used and non-self-explanatory notation that's a problem. You can achieve the same with words by inventing your own words and demanding that everyone learn them to understand you.

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#15

Post by lomnakkus » Thu, Jan 29, 2015, 7:15 PM UTC

frankmcsherry wrote: post #8

lomnakkus wrote: post #5

Could 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/18382…

Very interesting, thanks (and to the other sibling poster).

> Tom's TLA+ version was closing in on 200 pages, available at [snip]

This is one of those things that I forgot to mention, namely the sheer amount of ambient knowledge we have embedded in our (not our computer's!) background knowledge of math and logical reasoning. Of course, sometimes we're actually wrong, so maybe we could stand a little double-checking by computer-based proof assistants, but I digress...

One thing that's also been mentioned in previous discussions I've been involved in and which is slightly worrying is that these kinds of languages tend to be quite anti-modular in that the proofs required for one type of system often don't transfer very well to other types of systems. (In general "algebra" proofs should probably transfer pretty well, but we're usually interested in very specific proofs for our systems.)

Aside: I wonder if Russel & Whiteheads's classic 1+1 proof has yet been (computer-)formalized?

EDIT: Russel & Whitehead

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#16

Post by ipsum2 » Thu, Jan 29, 2015, 7:29 PM UTC

madsravn wrote: post #9

I just finished a course in Coq - it was pretty fun. Seems like something of the same the guys paper is about.

The article has nothing to do with Coq:

> When I saw the title of the talk, I assumed Lamport would be talking about computer proof checking programs or even a proof creating program like the one Timothy Gowers has worked on and written about. But Lamport’s advice was much more down-to-earth.

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#17

Post by Crito » Thu, Jan 29, 2015, 7:35 PM UTC

putzdown wrote: post #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).

A combination of both, something like Knuth's idea for Literate Programming, would be the best I think. Of course that would be way more work for whoever has to type it all up, so I don't think it has much of a chance to catch on.

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#18

Post by bsdetector » Thu, Jan 29, 2015, 7:38 PM UTC

putzdown wrote: post #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).

I'd say the problem with math notation is that it simply has too many symbols. It has a different symbol for everything because it was designed as a handwritten system.

For you mathematicians, think what you would do if you woke up tomorrow and all the math symbols had been replaced with emoji? I think most normal people would just learn the four operators and that's all... you know: megaphone, pizza slice, backpack, and recycle.

Math is what it is, designed for a pre-computer world, but what really kills me is when programmers use untypeable symbols like α (alpha), which at least is an actual letter in one language, or worse yet random unicode like · ("middle dot") or ∕ (division sign, not /). There's just no excuse for that.

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#19

Post by mjb » Thu, Jan 29, 2015, 7:43 PM UTC

lomnakkus wrote: post #5

Could 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…

We use it at Amazon Web Services (http://research.microsoft.com/en-us/um/people/lamport/tla/am...) and have found it very practically useful.

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#20

Post by xamuel » Thu, Jan 29, 2015, 7:44 PM UTC

bsdetector wrote: post #18

putzdown wrote: post #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).

I'd say the problem with math notation is that it simply has too many symbols. It has a different symbol for everything because it was designed as a handwritten system. For you mathematicians, think what you would do if you woke up tomorrow and all the math symbols had been replaced with emoji? I think most normal people would just learn the four operators and that's all... you know: megaphone, pizza slice, backpack,…

The reason for using different scripts (Greek etc.) is to sort symbols by broad categories. Done right, it actually makes things more readable (to the sophisticated reader, which is the mathematician's target audience anyway). It's almost like an implicit type system: (within a particular context) Greek letters mean ordinals, lowercase Roman letters mean predicate logic variables, uppercase German letters mean universes... It would be much less fun, and much harder, to follow an intense mathematical work if the variables were all in the same font.