Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

Some math people I talked to found formal logic to be the hardest branch. Proofs about proofs are maddening. Reasing about reasoning and about things you can't reason about is tricky.

Programming--at a high level--is just this with different syntax. Actually, that's both a simplification and an exaggeration. However, Dijkstra was very interested in formal verification, and that really is very much like the study of formal logic.

More generally, the study of programming languages and semantics (which is probably most of what he meant by programming as a branch of mathematics) is very closely related to formal logic. And while I personally think it's not nearly as scary as people make it out to be--please don't be afraid of type theory and formal verification!--most people do find it somewhat difficult.



The first time I understood a formal proof was with Dijkstra:

http://www.cs.utexas.edu/~EWD/ewd13xx/EWD1311.PDF

He is an exceptionally sharp thinker who is able to communicate his thought process with clarity. Even if you don't follow the math you understand how certain proofs can be abstracted from proofs made earlier.

I think you are correct, Dijkstra was exceptionally interested in formal verification to the point where he wasn't willing to envision a computing world that was not formally verified. When he said that programming is more difficult to mathematics he was probably envisioning the problems of formal logic with increasingly sophisticated programming structures.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: