PROVING PROGRAMS:A NOBLE CAUSE

Fall semester is fast approaching, so I need to get back to thinking about what I can do with my senior project that might help my graduate school application. I'm taking a graduate software foundations class in the fall with Benajamin Pierce, and he has collected a list of great papers in programming languages (PL) research.

To begin to get an understanding of the field in general and where my interests for research could lie, I am going to read some of the classical papers first. I started by reading "An Axiomatic Basis for Computer Programming" by C.A.R. Hoare in 1962, and he described the importance of proving the correctness of programs, a major part of the PL field:

The cost of error in certain types of program may be almost incalculable - a lost spacecraft, a collapsed building, a crashed aeroplane, or a world war. Thus the practice of program proving is not only a theoretical pursuit, followed in the interests of academic respectability, but a serious recommendation for the reduction of the costs associated with programming error.

Hoare goes on to outline that proving correctness of programs will solve three of the most serious problems in computer programming: reliability, documentation, and compatibility.

Sounds like a very good cause. Maybe I'll go work on that.