From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: * X-Spam-Status: No, score=1.4 required=5.0 tests=AWL,NO_REAL_NAME,SPF_FAIL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from discorde.inria.fr (discorde.inria.fr [192.93.2.38]) by yquem.inria.fr (Postfix) with ESMTP id 33AE2BC99 for ; Thu, 1 Feb 2007 06:05:55 +0100 (CET) Received: from selenite.metnet.navy.mil (selenite.metnet.navy.mil [192.16.167.32]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l1155qtV029511 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=FAIL) for ; Thu, 1 Feb 2007 06:05:54 +0100 Received: (qmail 4068 invoked by uid 107); 1 Feb 2007 05:05:51 -0000 Received: from unknown (HELO Adric.metnet.fnmoc.navy.mil) (10.100.105.102) by selenite.metnet.navy.mil with SMTP; 1 Feb 2007 05:05:51 -0000 Received: by Adric.metnet.fnmoc.navy.mil (Postfix, from userid 760) id E278AAB40; Wed, 31 Jan 2007 21:04:31 -0800 (PST) To: caml-list@inria.fr, Andrej.Bauer@fmf.uni-lj.si Subject: Programming with correctness guarantees Reply-To: oleg@pobox.com Errors-To: oleg@okmij.org From: oleg@pobox.com Message-Id: <20070201050431.E278AAB40@Adric.metnet.fnmoc.navy.mil> Date: Wed, 31 Jan 2007 21:04:31 -0800 (PST) X-Miltered: at discorde with ID 45C17530.001 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; oleg:01 andrej:01 tackled:01 booktitle:01 larus:01 abadi:01 pubs:01 kieburtz:01 ogi:01 pacsoft:01 mart:98 murphy:98 989:98 2002,:98 wrote:01 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.