9 Aug 2002 mslicker   » (Journeyer)

Formal methods and Dijkstra

I read through many of Dijkstra's papers recently. I have to agree with much of what he has said.

The skills to write good mathematical proofs and good programs are the same. And also, from experience, my math classes have been far more valuable than my computer science classes (with some exceptions). He said computer science students should be diciplined in mathematics and I think he is right.

Also he has said some things about elegance and simplicity. In math generally the more elegant and simple proofs are the ones that are taught. One math teacher of mine would give solutions. Somtimes people would turn in ten pages of proofs for an assignment. When he handed out his solutions the proofs fit on exactly one page. Programming problems also admit many solutions, and we should try to find the most elegant simple method of solving them.

Formal methods could be useful in programming, but not as a mechanical device to automatically check the correctness of your program. The key I think is developing highley modular programs. It is easy to check the correctness of a short function, you can even do it mentally. When functions get long, that is when you must get out the pencil and paper and follow each step.

Also the simpler a program is, the easier to check it's correctness. Often the problem we are addressing is one of our own choosing. Redefining the problem can often lead to simpler programs, and ones which are much easier to verify. This is a tremendous advantage which is often ignored in writing programs.

tk

Glad to stop. Our debate was turning more into an argument. I like debates, but not arguments.

Also I like to say that I don't care what programming language people use. I would much rather create than criticize. My remarks on C are mostly prompted by current attempts to parse it, which have taken far more work than I would like.

Latest blog entries     Older blog entries

New Advogato Features

New HTML Parser: The long-awaited libxml2 based HTML parser code is live. It needs further work but already handles most markup better than the original parser.

Keep up with the latest Advogato features by reading the Advogato status blog.

If you're a C programmer with some spare time, take a look at the mod_virgule project page and help us with one of the tasks on the ToDo list!