From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham
	autolearn_force=no version=3.4.4
X-Google-Thread: a07f3367d7,6327f05d4989a68d
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII-7-bit
X-Received: by 10.181.13.205 with SMTP id fa13mr9908777wid.3.1356837413503;
        Sat, 29 Dec 2012 19:16:53 -0800 (PST)
MIME-Version: 1.0
Path: 
 i11ni337233wiw.0!nntp.google.com!feeder3.cambriumusenet.nl!82.197.223.108.MISMATCH!feeder2.cambriumusenet.nl!feed.tweaknews.nl!85.12.40.139.MISMATCH!xlned.com!feeder7.xlned.com!newsfeed10.multikabel.net!multikabel.net!newsfeed20.multikabel.net!border3.nntp.ams.giganews.com!border1.nntp.ams.giganews.com!border4.nntp.ams.giganews.com!border2.nntp.ams.giganews.com!nntp.giganews.com!newsreader4.netcologne.de!news.netcologne.de!news.mixmin.net!newsfeed.straub-nv.de!reality.xs3.de!news.jacob-sparre.dk!munin.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail
From: "Randy Brukardt" <randy@rrsoftware.com>
Newsgroups: comp.lang.ada
Subject: Re: compilers,
 was Re: Press Release - Ada 2012 Language Standard Approved by ISO
Date: Thu, 27 Dec 2012 16:00:06 -0600
Organization: Jacob Sparre Andersen Research & Innovation
Message-ID: <kbigdg$qvp$1@munin.nbi.dk>
References: <kbg9bp$a72$1@munin.nbi.dk> <kbia4b$srn$1@speranza.aioe.org>
NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net
X-Trace: munin.nbi.dk 1356645617 27641 69.95.181.76 (27 Dec 2012 22:00:17 GMT)
X-Complaints-To: news@jacob-sparre.dk
NNTP-Posting-Date: Thu, 27 Dec 2012 22:00:17 +0000 (UTC)
X-Priority: 3
X-MSMail-Priority: Normal
X-Newsreader: Microsoft Outlook Express 6.00.2900.5931
X-RFC2646: Format=Flowed; Original
X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157
Date: 2012-12-27T16:00:06-06:00
List-Id: <comp.lang.ada>

<tmoran@acm.org> wrote in message news:kbia4b$srn$1@speranza.aioe.org...
>> I realize that the quality of proof needed to make this work might be
>> beyond the state-of-the-art today, but I doubt that will be the case by
>> the time a new version of Ada is defined.
>    I thought compilers were getting wider - handling more constructs -
> rather than deeper - more analysis and optimization.  Is that not the 
> case?

A compiler-writer that isn't making their code better is just going through 
the motions, IMHO. Optimization/code generation is the fun/rewarding part of 
compiler construction -- the rest of it is the busy work needed to support 
the fun. As such, I can't quite imagine a developer that takes pride in 
their work not trying to make that better.

And of course, the best way to generate faster checks is to prove that 
they're not needed at all. The fastest check is always the one you don't 
make! So more proof directly aids that primary goal of compiler writers. 
(For Ada, of course, it also offers the possibility of detecting more errors 
early.)

                                                      Randy.