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!feeder.eternal-september.org!newsfeed0.kamp.net!newsfeed.kamp.net!fu-berlin.de!uni-berlin.de!individual.net!not-for-mail
From: "Pascal J. Bourguignon" <pjb@informatimago.com>
Newsgroups: comp.lang.ada
Subject: Re: Heartbleed
Date: Sat, 12 Apr 2014 21:18:08 +0200
Organization: Informatimago
Message-ID: <877g6u4arz.fsf@kuiper.lan.informatimago.com>
References: <1ljwj8f.1wqbhvuabsdw1N%csampson@inetworld.net>
	<51c7d6d4-e3be-44d5-a4ce-f7e875345588@googlegroups.com>
	<li9g34$9q8$1@dont-email.me> <%J32v.70539$kp1.45343@fx14.iad>
	<liap70$ckq$1@speranza.aioe.org>
	<87mwfq4vvj.fsf@kuiper.lan.informatimago.com>
	<lymwfqo0j4.fsf@pushface.org>
	<87eh124awq.fsf@kuiper.lan.informatimago.com>
Mime-Version: 1.0
Content-Type: text/plain
X-Trace: individual.net NAfBDHaX5QUsv+FjH+Cg/wgKc6C/bQvINfyj+nsOBfrrHBqraI
Cancel-Lock: sha1:MmNjMTNlZDAzNzAyZWVjNjE5ZjZkNjA3YzJlNmZmMTQ2M2UwYjZmZA==
 sha1:rQZ5cfZXcbgDHQqTeJcQLvZVsCc=
Face: iVBORw0KGgoAAAANSUhEUgAAADAAAAAwAQMAAABtzGvEAAAABlBMVEUAAAD///+l2Z/dAAAA
      oElEQVR4nK3OsRHCMAwF0O8YQufUNIQRGIAja9CxSA55AxZgFO4coMgYrEDDQZWPIlNAjwq9
      033pbOBPtbXuB6PKNBn5gZkhGa86Z4x2wE67O+06WxGD/HCOGR0deY3f9Ijwwt7rNGNf6Oac
      l/GuZTF1wFGKiYYHKSFAkjIo1b6sCYS1sVmFhhhahKQssRjRT90ITWUk6vvK3RsPGs+M1RuR
      mV+hO/VvFAAAAABJRU5ErkJggg==
X-Accept-Language: fr, es, en
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/24.3 (gnu/linux)
Xref: news.eternal-september.org comp.lang.ada:19277
Date: 2014-04-12T21:18:08+02:00
List-Id: <comp.lang.ada>

"Pascal J. Bourguignon" <pjb@informatimago.com> writes:

> There will always be bugs remaining, even in tested and more
> importantly, even in proven software!  Cf. for example, the Deep Space 1
> RAX software, written in Lisp, and proven!  Despite the proof, a bug
> remained.  If it had been a statically checked programming language, it
> would have meant a terminal dead-lock or a crash (what else to do with a
> static language when we reach a state that has been proved impossible?).
> But since it was a dynamic programming language, (with very late
> binding, including a on-board compiler), it was debugged and patched
> remotely, as a last ressort solution.

Reference:

Formal Analysis of the Remote Agent Before and After Flight
http://spinroot.com/spin/Doc/rax.pdf

-- 
__Pascal Bourguignon__
http://www.informatimago.com/
"Le mercure monte ?  C'est le moment d'acheter !"