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
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: Simon Wright <simon@pushface.org>
Newsgroups: comp.lang.ada
Subject: Re: The future of Spark . Spark 2014 : a wreckage
Date: Wed, 10 Jul 2013 17:02:46 +0100
Organization: A noiseless patient Spider
Message-ID: <lyehb6wggp.fsf@pushface.org>
References: <d84b2eb2-eab3-4dec-917c-0498473c1e93@googlegroups.com>
	<krfb56$332$1@loke.gir.dk>
	<7ebe0439-fa4c-4374-a6c7-365ac78e6e39@googlegroups.com>
Mime-Version: 1.0
Content-Type: text/plain
Injection-Info: mx05.eternal-september.org;
 posting-host="c8504a89c76ea11bda6664e6198ae3cd";
	logging-data="1906"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX190eJ8HqO1zWIAMc9ddBmJ2ZhY0gw2Ewww="
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/24.3 (darwin)
Cancel-Lock: sha1:y3jhJ8peH5yNGL3/3tjYyYN+0+U=
	sha1:QcAqtsAr5ArCkPG7GWX8CRta2Ak=
Xref: news.eternal-september.org comp.lang.ada:16268
Date: 2013-07-10T17:02:46+01:00
List-Id: <comp.lang.ada>

vincent.diemunsch@gmail.com writes:

> Spark imposes static memory allocation to be able to prove total
> correctness, which means that the program will always do what is
> expected, which is required by embedded softwares...

Not at all sure that's true! Safety-related, security-related: probably,
other fields, not so much.

I just saw the Tony Hoare quote from 1995 (3rd quotation of [1]):

   "Ten years ago, researchers into formal methods (and I was the most
   mistaken among them) predicted that the programming world would
   embrace with gratitude every assistance promised by formalisation to
   solve the problems of reliability that arise when programs get large
   and more safety-critical. Programs have now got very large and very
   critical -- well beyond the scale which can be comfortably tackled by
   formal methods. There have been many problems and failures, but these
   have nearly always been attributable to inadequate analysis of
   requirements or inadequate management control. It has turned out that
   the world just does not suffer significantly from the kind of problem
   that our research was originally intended to solve."

[1] http://en.wikipedia.org/wiki/Tony_Hoare#Quotations