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

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#31

Post by pascal_cuoq » Thu, Jan 29, 2015, 9:10 PM UTC

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…

I have seen another instance of the talk summarized in the article. It is about machine-checked proofs (and even if you haven't seen the talk, have you seen who is giving it?). You won't see “huge leaps and unstated assumptions” in that format, although unimportant details may be relegated to fourth-level indentation or prelimary lemmas.

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#32

Post by _ikke_ » Thu, Jan 29, 2015, 9:13 PM UTC

threatofrain wrote: post #27

Chinjut wrote: post #25

Earlier quoted context omitted.

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.

How do you prevent discrapencies between those? You already see it with comments on source code, which eventually get outdated.

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#33

Post by AnimalMuppet » Thu, Jan 29, 2015, 9:15 PM UTC

tormeh wrote: post #14

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.

Which is just about the same as using a notation and demanding that everyone use the notation to understand you - except that a large number of people already know the notation.

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#34

Post by madsravn » Thu, Jan 29, 2015, 9:15 PM UTC

ipsum2 wrote: post #16

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.

I'm a referring the guys paper, which is linked here in the comments somewhere. There TLA+ is mentioned which is a tool to formally prove something. The same can be done in Coq - which is why I'm drawing a parallel.

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#35

Post by avodonosov » Thu, Jan 29, 2015, 9:17 PM UTC

Leslie Lamport is on this "how to write a proof" subject for long time. At least from 1995: http://research.microsoft.com/en-us/um/people/lamport/pubs/p...

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#36

Post by enupten » Thu, Jan 29, 2015, 9:19 PM UTC

To be fair, Leslie Lamport is also a Mathematician (his PhD was in Math).

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#37

Post by kazinator » Thu, Jan 29, 2015, 9:19 PM UTC

> He says that once you have a hierarchical proof, you can use pieces of it in new proofs very easily. For example, if you want to change one assumption slightly or focus on solutions that have different properties, you will be able to tell very easily which parts of the proof can stay the same and which parts will need to change.

If only that were true of a piece of LaTeX moved from one place to another, haha!

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#38

Post by lomnakkus » Thu, Jan 29, 2015, 9:23 PM UTC

ahelwer wrote: post #10

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'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 desi…

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

This sounds very intriguing. It guess there's at least some learning curve, but maybe it'll be a fun experiment vs. P&P in future. ;)

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#39

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

_ikke_ wrote: post #32

threatofrain wrote: post #27

Earlier quoted context omitted.

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.

How do you prevent discrapencies between those? You already see it with comments on source code, which eventually get outdated.

I think the answer to this, if my experience as a maintenance programmer is worth anything, is: don't trust the prose. Trust the code (proof). This is why strong type systems are so insanely valuable in programming, especially if they encode proofs of side effects or lack thereof.

Maybe there's a sort of golden middle way here where all mathematical prose-proofs should be annotated[1] by the associated computer-checked proof. The trustworthiness of a particular proof could be assessed by the number of such references and how much coverage (of the prose) they provide...?

[1] Perhaps only by reference, as here. :)

EDIT: Quick edit, I say this as someone who -- earlier in xir career -- probably subjected a lot of people to somewhat verbose comments. In practice, my comments were usually right and the programming language wasn't powerful enough to capture the semantics of what I was doing. One hopes this is the distinction between good and bad comments. Sorry for veering off-topic.

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#40

Post by avmich » Thu, Jan 29, 2015, 9:34 PM UTC

enupten wrote: post #36

To be fair, Leslie Lamport is also a Mathematician (his PhD was in Math).

And "computer science is one of the hardest branches of applied mathematics" (who's the author? Did Dijkstra said something like that?), so Lamport is in his own field.