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: Tue, 9 Jul 2013 09:28:56 +0200 Organization: cbb software GmbH Message-ID: <1vc73wjwkqmnl$.gx86xaqy60u4$.dlg@40tude.net> References: 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:16187 Date: 2013-07-09T09:28:56+02:00 List-Id: 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. > 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. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de