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 X-Received: by 10.180.210.168 with SMTP id mv8mr7367941wic.0.1373372554847; Tue, 09 Jul 2013 05:22:34 -0700 (PDT) X-FeedAbuse: http://nntpfeed.proxad.net/abuse.pl feeded by 78.192.65.63 Path: border1.nntp.dca3.giganews.com!border3.nntp.dca.giganews.com!border1.nntp.dca.giganews.com!nntp.giganews.com!cw2no9035920wib.0!news-out.google.com!md6ni50654wic.0!nntp.google.com!feeder1-2.proxad.net!proxad.net!feeder1-1.proxad.net!nntpfeed.proxad.net!news.muarf.org!news.ecp.fr!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: Tue, 9 Jul 2013 14:22:33 +0200 Organization: cbb software GmbH Message-ID: 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 X-Complaints-To: abuse@aioe.org User-Agent: 40tude_Dialog/2.0.15.1 X-Notice: Filtered by postfilter v. 0.8.2 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit X-Original-Bytes: 2756 Xref: number.nntp.dca.giganews.com comp.lang.ada:182375 Date: 2013-07-09T14:22:33+02:00 List-Id: On Tue, 09 Jul 2013 12:29:03 +0100, Simon Wright wrote: > "Dmitry A. Kazakov" writes: > >> On Mon, 8 Jul 2013 16:32:21 -0500, Randy Brukardt wrote: > >>> 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. > > I think what Randy meant (and may even have said) was that in > > with A; > package B is ... > > it shouldn't be necessary to look at the body of A to prove the body of > B. Of course the body of A will have to be proved ... but not right now. Yes this is how I understood him and what I objected to. You cannot rely on the contracts when it comes to correctness. OK, for the sake on the argument, you could contract proofs about A's body, so that these proofs could be used in the proofs of the body B. But the problem with that is exactly what Randy wanted to avoid - tight coupling and doing things in advance which nobody would ever needed. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de