The Science of Programming : Why be correct?

This post discuss the importance of The Science of Programming and why one should prove a program correct rather than conclude correctness from a few test cases.

module SoP0 where

This post is the start of a series on The Science of Programming, for which I am following the wonderfully written book of the same name by David Gries. As such all quotes, unless cited otherwise, originate from there. Among other things, the purpose is to view programming as a science: ‘practical work which depends on the knowledge and conscious application of principles.’

Setting

Suppose at some point, in a large program, you encounter a block of code that only makes sense —ie is well-defined: terminates, no division by zero errors, etc.– if some condition —ie Boolean expression of the variables involved— G is satisfied; moreover, you know that that the block of code performed as desired if some condition E is established.

You could just print output of the variable values and conditions of interest, then manually check, or assert, them to be true.

However, some compilers come with so-called ‘assert’ commands: ‘’if a Boolean expression appears between braces { and } at a point in the program, then whenever’‘flow of control’‘reaches that point during execution, it is checked: a message and a dump of of the program variables are printed; if true, execution continues normally.’‘—when efficiency is a concern, assertion statements can be tuned off: the compiler just ignores them. Sometimes these are known as ’code contracts’.

Now the problem: how do we know if our assertions G and E are what we need? Is it an ad-hoc process —a case-by-case approach? Is it trial and error? Well, such assertions specify, or define, what the code block was supposed to do, and so should have been written before writing the program segment. * So we turn an informal specification into a formal one, with Boolean expressions, of givens E and desired establishments E, then we look to develop a program S solving the equation {G} S {E}.*

‘’The study of program correctness proofs has led to the discovery and elucidation of methods for developing programs. Basically, one attempts to develop a program and its proof hand-in-hand, with proof ideas leading the way! If the methods are practised with care, they can lead to programs that are free of errors, that take much less time to develop and debug, and that are much more easily understood (by those who have studied the subject). … We should run test cases not to look for bugs, but to increase our confidence in a program we are quite sure is correct; finding an error should be the exception rather than the rule.’’ (SoP, p5)

What I am doing

When a student learns about the science of programming, one uses a minimalistic language and the associated proofs are not terribly informal: they are set within the domain of calculational mathematics. However, we are human and so are bound to make mistakes: is an expression well-defined, is a proviso met when applying a rule, is a theorem applied correctly. As such, one has peers review such proofs. My goal is to embed the minimalistic language introduced in Gries’ SoP into Agda such that the proofs presented in his text can be rendered nearly identically —due to the Unicode mixfix lexems of Agda— but also have the proofs type checked!

Things to consider

• “… a glimpse of the educational challenge we are facing: besides teaching technaalities, we have to overcome the mental resistance always evoked when it is shown how the techniques of scientific thought can be fruitfully applied to a next area of human endeavour. (We have already heard all the objections, which are so traditional they could have been predicted: ‘’old programs’‘are good enough,’‘new programs’‘are no better and are too difficult to design in realistic situations, correctness of programs is much less important than correctness of specifications, the’‘real world’‘does not care about proofs,…’’ –Edsger Dijkstra, Foreword of SoP

• ‘’New formalisms are always frightening, and it takes much careful teaching to convince the novice that the formalism is not only helpful but even indispensable.’’ –Edsger Dijkstra, Foreword of SoP

• Beginners to a formal approach complain that it only covers small problems, however since every large program consists of many small programs, Gries says: one cannot learn to write large programs effectively until one has learned to write small ones effectively.