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!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!nntp-feed.chiark.greenend.org.uk!ewrotcd!reality.xs3.de!news.jacob-sparre.dk!loke.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail From: "Randy Brukardt" Newsgroups: comp.lang.ada Subject: Re: The future of Spark . Spark 2014 : a wreckage Date: Wed, 17 Jul 2013 18:26:31 -0500 Organization: Jacob Sparre Andersen Research & Innovation Message-ID: 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> <1awbjaens2vca$.1asmpnthmmycl.dlg@40tude.net> NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net X-Trace: loke.gir.dk 1374103592 4337 69.95.181.76 (17 Jul 2013 23:26:32 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Wed, 17 Jul 2013 23:26:32 +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:16399 Date: 2013-07-17T18:26:31-05:00 List-Id: "Dmitry A. Kazakov" wrote in message news:1awbjaens2vca$.1asmpnthmmycl.dlg@40tude.net... > 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). Ah, you've redefined Ada's terms again. "Static" is defined in RM 4.9, and that's how I'm using it. "Proof", which is not an Ada concept, is not relevant to it's description. By your twisted definition, everything is static (including dynamic constraints!) if sufficient information is known at compile-time to reason about them. It would be nice to have a discussion where you didn't change the terminology from that accepted by Ada (this is, after all, an Ada group). ... >> 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. Nothing that has body dependencies can be integrated into Ada. ... >> 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. Absolutely. The sorts of proofs you want would absolutely kill program maintenance, making it impossible to have the sort of reusable libraries that Ada makes so easy. The contract represented by the interface can be the *only* thing that clients depend upon. If they depend on anything else, changes to the body will break otherwise correct calls, and that's unacceptable. This property if absolutely required to build large programs with large and distributed teams -- otherwise, "proof" remains solely the provence of small, toy-sized programs. > 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." You can only provide exception contracts if you have strong preconditions and constraints on the parameters. In the absense of that, you shouldn't be *allowed* to prove anything, because in doing so you force a strong coupling to the contents of the body. ... >>> 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. Nice theory, impossible to do in practice. Next suggestion... >> 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. It's impractical to have an Open that somehow encodes every possible sequence of Open-fall back-Open-Create that might come up. In the absense of that, you have to resort to complex program structures (it's not possible to declare objects with the right scope easily) or worse, lots of allocated objects. (A major cause of "allocator mania" is certain other languages is that they don't have sufficiently powerful ways to create stack objects.) In any case, we're talking about Ada here, and the form of Ada's I/O is fixed. The question is what proof techniques we can bring to these existing libraries, not how they could be designed in some hypothetical and unimplementable language. Randy.