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: border1.nntp.dca3.giganews.com!border2.nntp.dca3.giganews.com!border4.nntp.dca.giganews.com!border2.nntp.dca.giganews.com!nntp.giganews.com!usenet.blueworldhosting.com!feeder02.blueworldhosting.com!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, 10 Jul 2013 18:21:33 -0500 Organization: Jacob Sparre Andersen Research & Innovation Message-ID: References: <1vc73wjwkqmnl$.gx86xaqy60u4$.dlg@40tude.net> <6pqhcwi0wuop.15v6h3g7gkto4.dlg@40tude.net> NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net X-Trace: loke.gir.dk 1373498494 16137 69.95.181.76 (10 Jul 2013 23:21:34 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Wed, 10 Jul 2013 23:21:34 +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 X-Original-Bytes: 4503 Xref: number.nntp.dca.giganews.com comp.lang.ada:182449 Date: 2013-07-10T18:21:33-05:00 List-Id: "Dmitry A. Kazakov" wrote in message news:6pqhcwi0wuop.15v6h3g7gkto4.dlg@40tude.net... > On Tue, 9 Jul 2013 15:37:10 -0500, Randy Brukardt wrote: > >>> There are obviously goals which cannot be proven without the bodies. >>> Proofs >>> about specifications are important but far not all. Consider LSP as an >>> example. You cannot prove substitutability from interfaces. It simply >>> does >>> not work. Same with almost everything else, because proving something in >>> general is much more harder, even impossible, than proving things about >>> a >>> concrete instance, e.g. body. >> >> My contention is such things are not worth proving. With strong enough >> contracts (including class-wide contracts for dispatching calls, and >> contracts on subprogram types :-), important properties of code can be >> proven. > > No, that is the problem. You want to overburden the contracts with stuff > that does not belong there. This would make the design fragile. > > Consider as an example stack use. Do you want to contract all subprograms > to maximum stack use, or let the compiler to estimate stack use of a > concrete body? As I said, these sorts of things aren't worth proving. Certainly not until proof of simple concepts is already a widely used feature of Ada; then expanding it further might make sense. But we have to walk before we can run, and we're barely crawling right now. > Another example is a mathematical function like sine. In order to prove > its > correctness you would need an extremely elaborated apparatus of contract > specification which itself will be a source of countless bugs due to its > complexity. This is a typical over-specification. Only if somebody wanted > to verify an implementation of sine, he would have to look into the body. > Most people never will. There is no reason to prove such things. For things like Sine, the best one can do is copy an implementation from a cookbook -- it makes no sense to even imagine trying to create a new one. (That makes as much sense as creating a new sort.) Even the simplest tests will detect any implementation errors (and we're never going to be able to live without testing). ... >> What's too hard shouldn't be bothered with, because we've lived just >> fine with no proofs at all for programming up to this point. > > We didn't. Accessibility checks and constraint errors are a permanent > headache in Ada. Constraint_Errors a headache? They're a blessing, because the alternative is zillions of impossible to find bugs. (I lived with those in the early days of Janus/Ada; I'll never go back.) It will never, ever be possible to detect every runtime failure at compile-time, nor is it possible to pre-test because of the possiblity of race conditions, so we have to have Constraint_Error. It's annoying that one can't tell between specification errors that should be contracted and proved away and those that are truly runtime (that is, a normal part of the implementation); Ada does conflate these things and that's probably annoying to a purist. (You can't seem to see the difference, which leads to bizarre conclusions.) But it's far from fatal. Randy.