A Grand Challenge in Computing: Education Teaching Scientific Techniques of Software Development

The call for submissions suggests a theme for a Grand Challenge: Develop approaches to the teaching of Computing and supporting software in which the formal side is present but hidden and relegated (in the sense of being carried out automatically in the background) so that non-mathematicians can develop rigorous programs. We believe that this is simply neither attainable nor desirable. Relegating rigour to automated processes was only partly implied by the nature of the Grand Challenge issued by Professor Sir Tony Hoare at the Joint Modular Languages Conference 2003 (JMLC 2003), to develop a ‘verifying compiler ’ [1], which guarantees the correctness of a program before running it. He foresees that the development of such a compiler will be part of a larger effort in basing software development on scientific principles and he does not expect that the challenge to be achievable in the near future. Even if such automation is possible, the correctness of a program can in any case only be established with respect to its specification. This needs to be expressed in a form suitable for the automation process, so the programmer does not escape the need for rigour