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 X-FeedAbuse: http://nntpfeed.proxad.net/abuse.pl feeded by 78.192.65.63 Path: border1.nntp.dca3.giganews.com!border2.nntp.dca3.giganews.com!border4.nntp.dca.giganews.com!border2.nntp.dca.giganews.com!nntp.giganews.com!news.bbs-scene.org!de-l.enfer-du-nord.net!feeder1.enfer-du-nord.net!usenet-fr.net!proxad.net!feeder1-2.proxad.net!nntpfeed.proxad.net!news.muarf.org!news.ecp.fr!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: Tue, 9 Jul 2013 15:37:10 -0500 Organization: Jacob Sparre Andersen Research & Innovation Message-ID: References: <1vc73wjwkqmnl$.gx86xaqy60u4$.dlg@40tude.net> NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net X-Trace: loke.gir.dk 1373402231 6321 69.95.181.76 (9 Jul 2013 20:37:11 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Tue, 9 Jul 2013 20:37:11 +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: 3538 Xref: number.nntp.dca.giganews.com comp.lang.ada:182397 Date: 2013-07-09T15:37:10-05:00 List-Id: "Dmitry A. Kazakov" wrote in message news:1vc73wjwkqmnl$.gx86xaqy60u4$.dlg@40tude.net... > On Mon, 8 Jul 2013 16:32:21 -0500, Randy Brukardt wrote: > >>> I realy hope that Spark users will say to AdaCore that they aro going >>> wrong and that AdaCore will really try to make a better future for >>> Spark. >> >> Spark users are on a certain dead-end, IMHO. The future is getting proof >> into the hands of all programmers, as a normal part of their day-to-day >> programming. That requires that proofs aren't necessarily complete, > > Rather the programmer should announce what to prove and that proof must be > complete. Right. And that should be an integral part of compilation: no proof, no compilation. >> that >> they use whatever information is available, and most of all, that they >> only >> depend on the specifications of packages (never, ever, on the contents of >> a >> body). > > 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. 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. Proofs should be an aid to debugging, not the be-all, end-all. I want to add proof technology incrementally so that everyone can use a little of it, benefit from it, and then use more of it. It's how most Ada programmers learned to use types and constraints, and its the way to get proofs into the mainstream. Not by stand-alone tools and subsets with weird rules. Randy. Randy.