Programming with correctness guarantees

[oleg@pobox.com]

Andrej Bauer wrote:
> I would go further: it would be interesting to augment real programming
> languages with ways of writing specifications that can then be tackled
> by theorem provers and proof asistants.

Has been done, to a good effect. The following are three examples,
which use quasi-comments to add various correctness propositions to the
existing programming language. The first example, SPARK, has been used
for *large*, industrial projects, for quite some time.

@Book{		barnes-high,
  author	= "John Barnes",
  title		= "High Integrity Software: 
                    The {SPARK} Approach to Safety and Security",
  booktitle	= "High Integrity Software: 
                    The {SPARK} Approach to Safety and Security",
  year		= 2003,
  url		= "http://www.praxis-his.com/sparkada/sparkbook.asp 
                   http://www.praxis-his.com/sparkada/pdfs/sampler_final.pdf",
  isbn		= "0-321-13616-0",
}
The sample chapter is quite good.

@TechReport{	hunt-singularity,
  author	= "Galen Hunt and James R. Larus and Mart{\'\i}n Abadi and 
        Mark Aiken and Paul Barham and Manuel F{\"a}hndrich and
        Chris Hawblitzel and Orion Hodson and Steven Levi and
        Nick Murphy and Bjarne Steensgaard and David Tarditi and
        Ted Wobber and Brian D. Zill",
  title		= "An Overview of the {S}ingularity Project",
  year		= 2005,
  month		= oct,
  number	= "MSR-TR-2005-135",
  url		= "http://research.microsoft.com/research/pubs/view.aspx?type=technical+report&id=989",
  abstract = "Singularity is a research project in Microsoft Research
that started with the question: what would a software platform look
like if it was designed from scratch with the primary goal of
dependability? Singularity is working to answer this question by
building on advances in programming languages and tools to develop a
new system architecture and operating system (named Singularity), with
the aim of producing a more robust and dependable software
platform. Singularity demonstrates the practicality of new
technologies and architectural decisions, which should lead to the
construction of more robust and dependable systems.",
}

@Misc{		kieburtz-p-logic,
  author	= "Richard B. Kieburtz",
  title		= "{P}-Logic: Property Verification for {H}askell Programs",
  year		= 2002,
  month		= "14~"  # aug,
  url		= "ftp://ftp.cse.ogi.edu/pub/pacsoft/papers/Plogic.pdf"
}

Why this isn't widespread? Certainly Praxis doesn't seem to complain
too much about that fact: they can charge basically anything they
want, given little competition. I remember reading somewhere that
after a division of Siemens applied this technique to a high assurance
project, they noted an exhilarating feeling of being able to program
without unit tests. The code was correct by construction.