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=unavailable autolearn_force=no version=3.4.4 Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!mx02.eternal-september.org!feeder.eternal-september.org!gandalf.srv.welterde.de!news.jacob-sparre.dk!loke.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail From: "Randy Brukardt" Newsgroups: comp.lang.ada Subject: Re: {Pre,Post}conditions and side effects Date: Thu, 7 May 2015 13:32:28 -0500 Organization: Jacob Sparre Andersen Research & Innovation Message-ID: References: <2430252d-52a1-4609-acef-684864e6ca0c@googlegroups.com> <0a718b39-ebd3-4ab5-912e-f1229679dacc@googlegroups.com> <9ee5e186-5aaa-4d07-9490-0f9fdbb5ca18@googlegroups.com> <87tww5296f.fsf@adaheads.sparre-andersen.dk> <871tj9dp5b.fsf@theworld.com> <1ftovlipftuej.p27p4vog2ka6.dlg@40tude.net> NNTP-Posting-Host: rrsoftware.com X-Trace: loke.gir.dk 1431023548 19738 24.196.82.226 (7 May 2015 18:32:28 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Thu, 7 May 2015 18:32:28 +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 Xref: news.eternal-september.org comp.lang.ada:25760 Date: 2015-05-07T13:32:28-05:00 List-Id: "Dmitry A. Kazakov" wrote in message news:1ftovlipftuej.p27p4vog2ka6.dlg@40tude.net... > On Thu, 07 May 2015 11:01:26 +0200, Georg Bauhaus wrote: >> On 06.05.15 23:07, Randy Brukardt wrote: >>> In order for proof to >>> be part of the compiler, the proof language has to be part of the >>> language. >> >> If the proof language is understood by the compiler, this does not >> require it to be compilable Ada, or efficiently computable (and >> terminating in time), I think? > > A compiler compiles, evidently... > > The fallacy of Randy's conclusion is different. A compiler need not to be > the compiler from single language. True enough. I was going to refute that in my original message, but I thought it would be rambling. I personally am from the camp that thinks that Ada is the best possible language for commicating anything. (Well, other than with other humans, but that's the fault of the humans and not the language. ;-) [That's certainly true of the expression syntax, there might be some room for improvement in declarations.] If something can't be expressed in Ada, it's not worth expressing (I see no value to incomputable things). > The proof language is another language. It cannot be same language because > that is inconsistent. I completely disagree here. If one is required to write separate proof instructions, hardly anyone would do it. After all, developing in Ada already has a reputation for being slow, doubling that time is never going anywhere outside of narrow niches. The value of proof, IMHO, is in finding runtime failures at compile time, both because that will generate better code, and because earlier detection of errors is better. (This becomes even more useful in the face of exception contracts, because absence of an exception is then either proved or the program is illegal.) That makes proof most valuable when applied to runtime checks, such as Ada 2012 assertions, or simply explicit code of a similar form. I don't find any value in proving the "correctness" of code (whatever that means), because the description of what the code does is going to be at least as complex as the code itself, and thus at least as susptible to errors. You end up writing the program twice in two different languages. That might have value in extreme circumstances (loss of life potential), but most programs are not like that (my spam filter, for example, or our Ada compiler). So one language for the majority of us doing "normal" things; perhaps two languages for extreme cases (but I'm not remotely interested in that - thinks like SPARK are terribly limiting). Randy.