Path: utzoo!utgpu!attcan!uunet!lll-winken!lll-lcc!ames!pasteur!ucbvax!husc6!spdcc!ima!compilers-sender
From: unido!gmdzi!jc@uunet.uu.net (Juergen Christoffel)
Newsgroups: comp.compilers
Subject: Re: Why Can't We Build a C Compiler?
Message-ID: <3134@ima.ima.isc.com>
Date: 5 Jan 89 13:33:47 GMT
References: <3112@ima.ima.isc.com>
Sender: compilers-sender@ima.ima.isc.com
Reply-To: unido!gmdzi!jc@uunet.uu.net (Juergen Christoffel)
Organization: GMD - Gesellschaft fuer Mathematik und Datenverarbeitung mbH
Lines: 28
Approved: compilers@ima.UUCP


  [...]
> [as well as the syntax]. This will increase the safety of compilers. In
> England they are working on a system which will produce and prove a compiler
> for a language specified in VDM [I think this is in connection with the
  [...]

Proving a compiler? OK, generating them by machine and checking them
out by machine will make them better or more reliable than a hand
written one once the generator/checker is working properly. But with
all those proofs done by machine: they will be valid only when the
program doing the proofs will be correct as well?! How do you proof
this? Where is the point where this 'bootstrapping' will start? Back
at set theory as the formal definitions of integer numbers?

========================================================================
  Juergen Christoffel, jc@gmdzi.UUCP, (++49 2241) 14-2421
  German National Research Laboratory for Computer Science (GMD)
  Schloss Birlinghoven, Postfach 1240, D-5205 St. Augustin 1, FRG
========================================================================
[Having tried to read the PL/I standard, I have to view with scepticism that
any formal specification of a non-trivial language could be credibly bug free,
at least using the kind of formalisms we have today.  -John]
--
Send compilers articles to ima!compilers or, in a pinch, to Levine@YALE.EDU
Plausible paths are { decvax | harvard | yale | bbn}!ima
Please send responses to the originator of the message -- I cannot forward
mail accidentally sent back to compilers.  Meta-mail to ima!compilers-request