Abstract
In the late 1960s people were talking about the promise of programs that verify the correctness of other programs. Unfortunately, it is now the middle of the 1980s, and, with precious few exceptions, there is still little more than talk about automated verification systems. Despite unrealized expectations, however, the research on program verification has given us something far more valuable than a black box that gobbles programs and flashes “good” or “bad”—we now have a fundamental understanding of computer programming.
The purpose of this column is to show how that fundamental understanding can help programmers write correct programs. But before we get to the subject itself, we must keep it in perspective. Coding skill is just one small part of writing correct programs. The majority of the task is the subject of the three previous columns: problem definition, algorithm design, and data structure selection. If you perform those tasks well, then writing correct code is usually easy.
Recommendations
The translation of 'go to' programs to 'while' programs
Classics in software engineeringSome of the papers presented in this book already have been widely circulated; others were published in well-known journals, like IBM Systems Journal but largely were ignored when they first appeared; and then there are the obscure papers like this one ...
Fifteen years of functional pearls
ICFP '06: Proceedings of the eleventh ACM SIGPLAN international conference on Functional programmingIn 1991, when the Journal of Functional Programming was inaugurated, the editors, Simon Peyton Jones and Philip Wadler, asked me to contribute a regular column to be called Functional Pearls. The idea was to emulate the very successful series of essays ...
Comments