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: 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!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, 10 Jul 2013 12:03:36 +0200 Organization: cbb software GmbH Message-ID: <6pqhcwi0wuop.15v6h3g7gkto4.dlg@40tude.net> References: <1vc73wjwkqmnl$.gx86xaqy60u4$.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 Xref: news.eternal-september.org comp.lang.ada:16255 Date: 2013-07-10T12:03:36+02:00 List-Id: 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? 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. Contracts should not define semantics, only most general properties of. Yet semantics should sometimes be proven. The provider does not know when. It is up to the user. In that case he have to look into the body. > 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. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de