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,FREEMAIL_FROM
	autolearn=unavailable autolearn_force=no version=3.4.4
X-Received: by 10.224.37.3 with SMTP id v3mr36794701qad.2.1373586608858;
        Thu, 11 Jul 2013 16:50:08 -0700 (PDT)
X-Received: by 10.50.4.99 with SMTP id j3mr19806igj.6.1373586608821; Thu, 11
 Jul 2013 16:50:08 -0700 (PDT)
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!news.bbs-scene.org!border4.nntp.dca.giganews.com!border2.nntp.dca.giganews.com!nntp.giganews.com!t19no1178403qam.0!news-out.google.com!f7ni2066qai.0!nntp.google.com!t19no1250687qam.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Thu, 11 Jul 2013 16:50:08 -0700 (PDT)
In-Reply-To: <krkums$ldf$1@loke.gir.dk>
Complaints-To: groups-abuse@google.com
Injection-Info: glegroupsg2000goo.googlegroups.com;
 posting-host=69.20.190.126;
 posting-account=lJ3JNwoAAAAQfH3VV9vttJLkThaxtTfC
NNTP-Posting-Host: 69.20.190.126
References: <d84b2eb2-eab3-4dec-917c-0498473c1e93@googlegroups.com>
 <krfb56$332$1@loke.gir.dk>
 <7ebe0439-fa4c-4374-a6c7-365ac78e6e39@googlegroups.com>
 <krkums$ldf$1@loke.gir.dk>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <290217ec-c2f5-4a34-b83f-ff743f355c7b@googlegroups.com>
Subject: Re: The future of Spark . Spark 2014 : a wreckage
From: Shark8 <onewingedshark@gmail.com>
Injection-Date: Thu, 11 Jul 2013 23:50:08 +0000
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: quoted-printable
Xref: news.eternal-september.org comp.lang.ada:16307
Date: 2013-07-11T16:50:08-07:00
List-Id: <comp.lang.ada>

On Wednesday, July 10, 2013 6:36:42 PM UTC-6, Randy Brukardt wrote:
>=20
> The idea of "total correctness" is exactly what I object to. It's a false=
=20
> promise that only works on tiny, toy programs. Real Spark programs almost=
=20
> always interface to "regular" Ada code to do stuff that Spark can't handl=
e,=20
> and once you've done that, you've lost your "total correctness".

Interesting sentiment, I'm not sure I agree with you -- though I can see wh=
at you're saying -- as a counter-example there's IRONSIDES, a DNS server th=
at is "provably exception-free, contains no data flow errors, and terminate=
s only in the ways that its programmers explicitly say that it can."

http://ironsides.martincarlisle.com/


I think we DO need "total correctness" in the lower levels of our software-=
stacks. Specifically OSes and compilers; I, for one, would love to see a pr=
oved Ada OS (no *nix, please) developed on a proved Ada compiler. -- I don'=
t *know* if that would be "in demand" by the industry (but then, the indust=
ry is embracing C-style languages and ramming their heads on the walls buil=
t by those misdesigns).