“KWARC was!”

Notes on Cristian S. Calude et al. (2007) Proving and Programming (see also previous post, see slides). Please note that the authors do not necessarily share my personal opinions and summaries on this page.

There is a strong analogy between proving theorems in mathematics and writing programs in computer science. Programming gives mathematics a new form of understanding. The computer is the driving force behind these changes.

• “Theorems (in mathematics) correspond to algorithms and not programs (in computer science)”
• “Programs (in computer science) correspond to mathematical models.”
• Proving the correctness of algorithms is seldom a focus in software projects (but: even testing/ documenting is sometimes neglected)
• Do some programming language facilitate/ required to put more focus on the correctness of the algorithms (e.g. functional language such as scala or ML; where programs are closer to mathematical models than in imperative languages)?
• Can bugs be avoided? Can the use of rigorous mathematical proofs guarantee that software and hardware perform as expected?
• Many projects and products dedicated to automated testing of program correctness, for example, VIPER or TestEra (automated testing of Java programs).
• What do proof obligations (Verpflichtung) have to do with the correctness of programs?: e.g. Barthe et al. discuss the “interaction between compilation and verification condition generators (VC generators), which are used in many interactive verification environments to guarantee the correctness of source programs, and by several proof carrying code (PCC) architectures to check the correctness of compiled programs. Such VC generators operate on annotated programs that carry loop invariants and procedure specifications expressed as preconditions and postconditions, and yield a set of proof obligations that must be discharged in order to establish the correctness of the program.” (loop and procedure level; see also specification languages such as CASL for the representation of precondition, invariants, and postconditions, i.e. proofs obligation)
• But correctness proof for a program, adds very little to one’s confidence in the program: “Beware of bugs in the above code: I have only proved it correct, not tried it. (Knuth)” (p.310)
• Checking new types of proofs: probabilistic, experimental, hybrid proofs (computation plus theoretical arguments) (p.311 ff.)

Further readings

• Hayashi (1998): Testing Proofs by Examples

This entry was posted on Tuesday, October 21st, 2008 at 2:43 am and is filed under CoPs in Math, Cristian Calude, University of Auckland. You can follow any responses to this entry through the RSS 2.0 feed. You can leave a response, or trackback from your own site.