Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

A Computer Scientist Tells Mathematicians How to Write Proofs

blogs.scientificamerican.com

Post reply on HN
Print view View original

21–30 of 103 posts

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#21

Post by lomnakkus »

mjb wrote: post #19
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.

Yes, thank you, that was very interesting and insightful -- I've read it before, in fact it sparked my initial interest in TLA+. Unfortunately this is not necessarily applicable for a "working programmer" aka "poor man without huge resources at his disposal". Maybe I should work on the latter problem and then start to apply TLA+. Or maybe it should be the other way 'round. :)

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#22

Post by vidarh »

The article starts with a false equivalence between archaic verbose language and mathematical notation.

For my part, I usually prefer the prose. Formulas are easier to read for people who are used to and have practice with mathematical notation, but even then they are easier to read for those people when they are sufficiently complete, and formulas seem to often come with huge leaps and unstated assumptions.

Especially in computer science papers I tend to see extensive use of formulas over prose or - preferably - code or pseudo-code as big warning signs: Often it turns out to mean the author is glossing over a massive amount of hugely important details. E.g. a common problem I saw when studying was papers that would describe processes, but omit any indications of sensible ranges for parameters that were essential to getting good results (I was working on techniques for image processing to improve OCR results), or greatly obscure details of algorithms that would have taken no more lines to write out in working code.

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#23

Post by gone35 »

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…

Interesting. So perhaps we need some sort of "CTLAN" (Comprehensive TLA+ Tautology Archive Network?) kind of thing to be able to import/match obligations to already-established proofs from some common repository? Maybe future versions of TLAPS would benefit from such a thing?

(Sorry if this already exists; I'm just an interested layman.)

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#25

Post by Chinjut »

vidarh wrote: post #22

The article starts with a false equivalence between archaic verbose language and mathematical notation. For my part, I usually prefer the prose. Formulas are easier to read for people who are used to and have practice with mathematical notation , but even then they are easier to read for those people when they are sufficiently complete , and formulas seem to often come with huge leaps and unstated assumptions. Especi…

Does prose not also often come with huge leaps and unstated assumptions?

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#27

Post by threatofrain »

Chinjut wrote: post #25
vidarh wrote: post #22

The article starts with a false equivalence between archaic verbose language and mathematical notation. For my part, I usually prefer the prose. Formulas are easier to read for people who are used to and have practice with mathematical notation , but even then they are easier to read for those people when they are sufficiently complete , and formulas seem to often come with huge leaps and unstated assumptions. Especi…

Does prose not also often come with huge leaps and unstated assumptions?

I think the solution is probably to have it all, according to your taste: code because you can run it as a working proof, and explanations in both comments and prose.

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#28

Post by bsdetector »

xamuel wrote: post #20
bsdetector wrote: post #18

Earlier quoted context omitted.

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

Yes that's the pre-computer I was talking about. Sophisticated mathematicians should be concerned about if it is machine readable or not. If it's machine readable then you can use whatever font, color, or any other style you want that helps you to read it. The viewer can abbreviate descriptive names to single glyphs if you want.

Programming is much less fun, and harder to follow, without syntax highlighting. But it doesn't follow that we should manually be color coding syntax and variables, or that integers should always be blue. That's essentially the case with the "readability" of mathematics.

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#29

Post by kriro »

I think the "you should try it either way since it may clarify your thought process or reveal problems" is important. It's often good to check your discoveries with different methods.

Of topic but in a similar vain: in a completely different field I dabble in reconstructing existing theories in structuralism. There's some very valid criticism of the method and yet it still unearths issues with theories every now and then.

http://en.wikipedia.org/wiki/Structuralism_%28philosophy_of_...

Post reply on HN