Re: Why Can't We Build a C Compiler?

unido!gmdzi!jc@uunet.uu.net (Juergen Christoffel)
5 Jan 89 13:33:47 GMT

          From comp.compilers
Related articles
[3 earlier articles]
Re: Why Can't We Build a C Compiler? henry@zoo.toronto.edu (1988-12-21)
Re: Why Can't We Build a C Compiler? nick@lfcs.ed.ac.uk (Nick Rothwell) (1988-12-20)
Re: Why Can't We Build a C Compiler? seanf@sco.uucp (1988-12-23)
Re: Why Can't We Build a C Compiler? daveb@lethe.uucp (1988-12-26)
Re: Why Can't We Build a C Compiler? olender@rachmaninov.CS.ColoState.EDU (1988-12-28)
Re: Why Can't We Build a C Compiler? frode@m2cs.naggum.se (Frode Odegard) (1988-12-29)
Re: Why Can't We Build a C Compiler? unido!gmdzi!jc@uunet.uu.net (1989-01-05)
Why can't we build a C compiler? think!compass!worley@EDDIE.MIT.EDU (1988-12-19)
Re: Why Can't We Build a C Compiler? jbs@fenchurch.mit.edu (1989-01-03)
Re: Why can't we build a C compiler? uokmax!glcowin@Central.Sun.COM (1989-01-18)
Re: Why can't we build a C compiler? limonce@pilot.njin.net (1989-01-24)
Re: Why can't we build a C compiler? waterloo.edu!cognos!rayt@RELAY.CS.NET (R.) (1989-01-25)
Re: Why can't we build a C compiler? kurt@tc.fluke.com (1989-01-25)
| List of all articles for this month |
From: unido!gmdzi!jc@uunet.uu.net (Juergen Christoffel)
Newsgroups: comp.compilers
Date: 5 Jan 89 13:33:47 GMT
References: <3112@ima.ima.isc.com>
Organization: GMD - Gesellschaft fuer Mathematik und Datenverarbeitung mbH

    [...]
> [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]
--

Post a followup to this message

Return to the comp.compilers page.
Search the comp.compilers archives again.