DC ACM

Program correctness is a scientific ideal for Computer Science, like accuracy of measurement is for physics, or purity of materials for Chemistry. It should be pursued independent of practical applications, exploiting scientific method to ensure that intermediate research results are cumulative. The research will answer the fundamental questions of software engineering such as 'What does a program do? How does it work? Why does it work? And how do we know that the answers to these questions are correct?' The research results should be incorporated in a research tool known as a program verifier. If the research is successful, its results should be transferred to software engineering practice, and contribute to saving a significant part of the current costs of programming error.