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!news.swapon.de!fu-berlin.de!uni-berlin.de!individual.net!not-for-mail From: Niklas Holsti Newsgroups: comp.lang.ada Subject: Re: {Pre,Post}conditions and side effects Date: Sat, 09 May 2015 08:18:37 +0300 Organization: Tidorum Ltd 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> <121ytg16vbxsk$.18dxo1h7daxty.dlg@40tude.net> Mime-Version: 1.0 Content-Type: text/plain; charset=windows-1252; format=flowed Content-Transfer-Encoding: 7bit X-Trace: individual.net 5fqHZfSda3ZKzQi4dA2ZDwdhcO7HLZyzEtWZAeV7MYxViQAMnM Cancel-Lock: sha1:UWhhtLNlXUqVCkiCVqFGKQH2Gbo= User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.8; rv:31.0) Gecko/20100101 Thunderbird/31.6.0 In-Reply-To: Xref: news.eternal-september.org comp.lang.ada:25785 Date: 2015-05-09T08:18:37+03:00 List-Id: On 15-05-09 02:16 , Randy Brukardt wrote: > "Niklas Holsti" wrote in message > news:cr1snsF60hoU1@mid.individual.net... >> On 15-05-07 22:01 , Randy Brukardt wrote: >>> wrote in message >>> news:alpine.DEB.2.11.1505071909280.16448@debian... >>> ... >>>> One property of a proper precondition (or postcondition or ...) is that >>>> disabling the check does not change the functional behaviour of correct >>>> programs. >>> >>> Sure, but this is irrelevant. There are no "correct" programs (in all >>> possible senses). How do you know that you have a correct program? If you >>> use some prover program, it too may have bugs. Or there might be bad data >>> (cosmic rays?) >> >> Those are practical problems, not problems of principle. If you would take >> the same attitude to mathematics, you would claim that there are no >> correct theorems. So I disagree with you. > > All programming is practical. We do not care about theorems, only that the > current program is correct in the current environment. You have lost me here: you want to make the compiler prove things, but you do not care about theorems, and do not want to be infected with a "theory" disease? Is Humpty Dumpty involved somehow, making words mean whatever he wants them to mean? :-) > Everything has to be reproved when anything changes Agreed. > (another good reason for putting it into the compiler, as skipping the step > isn't possible, and thus problems like the Ariene 5 don't happen). It is true that an optimizing and run-time-check-removing compiler has to make the same kind of analyses and have the same kind of understanding of the program's semantics as a program-proving tool. But constructing a proof from scratch is expensive, unpredictably expensive, and possibly non-terminating, while compilation of source code into machine code should take a time that is reasonable, and reasonably predictable. Hitherto, compilers have been expected to remove run-time checks that the compiler can prove to itself are redundant, but not to remove *all* redundant run-time checks. If the latter is required, compilation time becomes unlimited -- a practical problem, no? To make proof a routine part of compilation, it has IMO to be reduced to *proof checking*. Checking a proof is fast and terminating. To integrate proof-checking with compilation, the programming language has to be able to express the proof (axioms, lemmas, individual proof steps) interwined with the expression of the computation that is to be proved. And this has to be so easy that it tempts the programmer to write the proof -- or at least enough of the proof to guide the compiler -- as a routine part of creating the program. (Echoes here of proof-carrying code, http://en.wikipedia.org/wiki/Proof-carrying_code.) Ada has always had such features -- principally types, subtypes, ranges -- and Ada 2012 has added more -- pre/post-conds and invariants. However, I'm not sure if the features are yet sufficient to let us require, in the Ada standard, that an Ada compiler should be able to prove (rather, to check) exception-freeness, or termination, just to give two examples. I believe it is a good goal for evolving Ada, but of course not the only goal. By the way, if exception contracts are added to Ada, termination contracts should be considered, too. -- Niklas Holsti Tidorum Ltd niklas holsti tidorum fi . @ .