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=-0.3 required=5.0 tests=BAYES_00, REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4 Path: border1.nntp.ams3.giganews.com!border1.nntp.ams2.giganews.com!border3.nntp.ams.giganews.com!border1.nntp.ams.giganews.com!nntp.giganews.com!news.mixmin.net!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: The future of Spark . Spark 2014 : a wreckage Date: Wed, 17 Jul 2013 09:59:12 +0200 Organization: cbb software GmbH Message-ID: <1awbjaens2vca$.1asmpnthmmycl.dlg@40tude.net> References: <1vc73wjwkqmnl$.gx86xaqy60u4$.dlg@40tude.net> <6pqhcwi0wuop.15v6h3g7gkto4.dlg@40tude.net> <1s6sw93u97355$.1n0205ucj6251.dlg@40tude.net> <1lhsyg46iz9jj.8jrvydqxt8l6.dlg@40tude.net> <1d4tuwlfdnz2j$.18l68s96x3vjj.dlg@40tude.net> <1rjye7dyn3vgk.66fbcca9y4zd.dlg@40tude.net> Reply-To: mailbox@dmitry-kazakov.de NNTP-Posting-Host: IenaDxMXK2hi7fvYcb+MlQ.user.speranza.aioe.org Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit X-Complaints-To: abuse@aioe.org User-Agent: 40tude_Dialog/2.0.15.1 X-Notice: Filtered by postfilter v. 0.8.2 X-Original-Bytes: 7104 Xref: number.nntp.dca.giganews.com comp.lang.ada:182546 Date: 2013-07-17T09:59:12+02:00 List-Id: On Tue, 16 Jul 2013 17:13:43 -0500, Randy Brukardt wrote: > "Dmitry A. Kazakov" wrote in message > news:1rjye7dyn3vgk.66fbcca9y4zd.dlg@40tude.net... >> On Mon, 15 Jul 2013 19:13:24 -0500, Randy Brukardt wrote: >>> Ada compilers do it all the time. The issue is letting the programmer >>> have access to that information. >> >> This is upside down. The programmer should manifest his intention for a >> constraint to hold and the compiler should verify that. The manifest must >> be syntactically visible. Conflation such declaration with dynamic >> constraints is a bad idea. > > Yes, that's precisely what I'm talking about - some sort of exception > contract. But those don't depend on the kind of constraint. But they do, exception contract is a static constraint. It is no matter what is constrained, but how. Dynamically (=>code) vs. statically (=>proof). >>> In any case, going that route completely takes the compiler out of the >>> equation. Once you do that, only an extremely limited number of users >>> would care, and there will be no effect on normal programs. >> >> I disagree. I trust that most Ada programmers will enjoy trying it in their >> program and gradually relaxing requirements on the proofs as they see what >> can and what cannot be proved. > > No one is going to run extra tools beyond compilation; they simply don't > have the time. The "win" with Ada is that the extra correctness brought by > the language comes for "free", They aren't free as they rely on careful choice of types. This is indeed frustrating for must programmers with C and "everything is int" background. But Ada programmers are different, otherwise they weren't Ada programmers. > it's an integrated part of the development > process. (Your program cannot be run if it doesn't compile.) Extra tools > never will have that level force behind them, and people like me would never > run them. I always was for SPARK being integrated into Ada. >>> Why is there a problem? Every Ada compiler (and pretty much every other >>> compiler as well) does it already. >> >> How do you prove that this does not raise Constraint_Error >> >> function Geometric_Mean (A, B : Float) return Float is >> begin >> return sqrt (A * B); >> end Geometric_Mean; > > You can't, because it does. :-) Your contract is not strong enough, which is > not surprising: you have unbounded types here -- you can prove nothing about > such types. > > But that's OK, there is no point in proving everything about everything. > Moreover, if you made this an expression function (meaning that you are > merely giving a name to "sqrt (A*B)", you could plug it in without any > effect on your proof. Enjoy. But you could prove that with concrete ranges of A and B at the client side. Which is the whole point. You want to discard a whole class of proofs. Especially the ones crucial for exception contracts. How are you going to prove the caller's contract not to raise? You could not without non-sensual handlers. It would be like the idiotic "function must have a return statement rule." >>> The only issue is that programmers can't >>> harness it for their own purposes. I would hope that exception contracts >>> would be defined in order to do that. >> >> Yes. But they will only help if used on the client side and when bodies are >> looked into. > > You might be right, but in that case we're wasting our time even thinking > about proof, because any technology that requires programmer-visble access > to bodies is evil. ("Evil" here being a shorthand for "has a bunch of bad > properties", which I've previously outlined.) Yes of course. Just like Churchill's remark about democracy, it is evil, but anything else is much worse. Correctness proof has the nature similar to optimization, most powerful on concrete instances and close to damaging in general. >> 1. You will not prove that sqrt never raises Constraint_Error. You will do >> that in *your* calls to sqrt it never does. > > You don't have to. A properly written Sqrt has a precondition, and that > precondition raises Constraint_Error when it fails. Sqrt itself never raises > any exception. In most cases the precondition cannot be spelled or is more complex than the implementation itself. It is just a wrong (and not working) way to do this. >> Opening readonly file for writing is not a bug it is an error, a legitime >> state of the program which must be handled. Writing a file opened as >> readonly is a bug. Bug /= error. Errors are handled, bugs are fixed. > > You claim that you can use the file type to eliminate Status_Error and > Mode_Error. But that's impossible, because an Open that fails leaves the > file unopened; This is another issue, i.e. construction and initialization. You should not be able to create unopened instances of file type. > and you have to be able to fall back and open a different > file (or create one instead) on such a condition. It's not practical to have > a single Open operation as an initializer Why? I certainly want it exactly this way. >> I don't see how allowing correctness checks involving the bodies should >> prevent correctness checks involving the specifications. > > Because you can't have "correctness checks" involving bodies that don't > exist. Yes, it certainly will require some consideration of how to deal with opaque libraries. The model is already a bit leaky in GNAT which requires *.ali files. Maybe checks involving the bodies should be performed rather by the binder and the information required for that stored in the *.ali files or equivalent. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de