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.dca3.giganews.com!border2.nntp.dca3.giganews.com!border4.nntp.dca.giganews.com!border2.nntp.dca.giganews.com!nntp.giganews.com!nx02.iad01.newshosting.com!newshosting.com!news2.euro.net!feeds.phibee-telecom.net!de-l.enfer-du-nord.net!feeder2.enfer-du-nord.net!gegeweb.org!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: Thu, 11 Jul 2013 09:44:54 +0200 Organization: cbb software GmbH Message-ID: <1s6sw93u97355$.1n0205ucj6251.dlg@40tude.net> References: <1vc73wjwkqmnl$.gx86xaqy60u4$.dlg@40tude.net> <6pqhcwi0wuop.15v6h3g7gkto4.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: 3687 Xref: number.nntp.dca.giganews.com comp.lang.ada:182456 Date: 2013-07-11T09:44:54+02:00 List-Id: On Wed, 10 Jul 2013 18:21:33 -0500, Randy Brukardt wrote: > "Dmitry A. Kazakov" wrote in message > news:6pqhcwi0wuop.15v6h3g7gkto4.dlg@40tude.net... >> 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. Do you have Hankel function in your cookbook? How do you know that the copy you made is authentic? What is about the accuracy of the implementation? >>> 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. No, the alternative is to prove that the constraint is not violated. You can do this only at the client side. Which is why it cannot be contracted for the callee. When you move from instances to universally holding contracts you frequently lose provability. Note how accessibility checks attempted in the form of a contract became more problem than solution. In order to have it provable you must strengthen it. Probably every Ada programmer was annoyed by silly "must be statically deeper" messages about pointers. It cannot be handled at the level of contracts. Yet in most cases it is no problem to see that a *given* pointer is never dangling. > 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); That was ARG's decision for Ada 2012, wasn't it? > 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. It is fatal, because inconsistent. Error /= bug. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de