From owner-freebsd-hackers Wed Oct 9 15: 2:28 2002 Delivered-To: freebsd-hackers@freebsd.org Received: from mx1.FreeBSD.org (mx1.freebsd.org [216.136.204.125]) by hub.freebsd.org (Postfix) with ESMTP id 3DE6337B401; Wed, 9 Oct 2002 15:02:27 -0700 (PDT) Received: from boreas.isi.edu (boreas.isi.edu [128.9.160.161]) by mx1.FreeBSD.org (Postfix) with ESMTP id 75D8643E4A; Wed, 9 Oct 2002 15:02:26 -0700 (PDT) (envelope-from faber@ISI.EDU) Received: from pun.isi.edu (pun.isi.edu [128.9.160.150]) by boreas.isi.edu (8.11.6/8.11.2) with ESMTP id g99Lx2C12208; Wed, 9 Oct 2002 14:59:02 -0700 (PDT) Received: from pun.isi.edu (localhost [127.0.0.1]) by pun.isi.edu (8.12.6/8.12.6) with ESMTP id g99Lx1Pp085686; Wed, 9 Oct 2002 14:59:01 -0700 (PDT) (envelope-from faber@pun.isi.edu) Received: (from faber@localhost) by pun.isi.edu (8.12.6/8.12.6/Submit) id g99Lx1Kh085685; Wed, 9 Oct 2002 14:59:01 -0700 (PDT) Date: Wed, 9 Oct 2002 14:59:01 -0700 From: Ted Faber To: Terry Lambert Cc: "Nelson, Trent ." , "'hackers@freebsd.org'" , "'questions@freebsd.org'" Subject: Re: FreeBSD usage in safety-critical environments Message-ID: <20021009215900.GC93282@pun.isi.edu> References: <8F329FEDF58BD411BE5200508B10DA7607D71A10@exchptc1.switch.com> <3DA482D6.F618F6C5@mindspring.com> Mime-Version: 1.0 Content-Type: multipart/signed; micalg=pgp-sha1; protocol="application/pgp-signature"; boundary="mvpLiMfbWzRoNl4x" Content-Disposition: inline In-Reply-To: <3DA482D6.F618F6C5@mindspring.com> User-Agent: Mutt/1.4i X-url: http://www.isi.edu/~faber Sender: owner-freebsd-hackers@FreeBSD.ORG Precedence: bulk List-ID: List-Archive: (Web Archive) List-Help: (List Instructions) List-Subscribe: List-Unsubscribe: X-Loop: FreeBSD.ORG --mvpLiMfbWzRoNl4x Content-Type: text/plain; charset=us-ascii Content-Disposition: inline On Wed, Oct 09, 2002 at 12:26:14PM -0700, Terry Lambert wrote: > Life support systems require formal proofs of correctness for code; > since neither Linux nor FreeBSD is formally correct, in total, you > would need to be insane to deplaoy either of them as, for example, > a part of an air traffic control system. I suspect that's a bad example, or that you mean an embedded aircraft control system. Ron Reisman and James Murphy gave a fine invited talk at USENIX 02 (http://www.usenix.org/events/usenix02/tech/#11am) about the growing number of UNIX components in the US ATC system. I reject the conclusion that the FAA is collectively insane for that reason. ---------------------------------------------------------------------- Ted Faber faber@isi.edu USC/ISI Computer Scientist http://www.isi.edu/~faber (310) 448-9190 PGP Keys: http://www.isi.edu/~faber/pubkeys.asc --mvpLiMfbWzRoNl4x Content-Type: application/pgp-signature Content-Disposition: inline -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.0.7 (FreeBSD) iD8DBQE9pKakaUz3f+Zf+XsRApo2AJwMLYdFonRM4VfHSNZqePEF8Dny0ACfb6QJ 6u4wLjkoKK7+Hz8+XEP2+do= =wNh+ -----END PGP SIGNATURE----- --mvpLiMfbWzRoNl4x-- To Unsubscribe: send mail to majordomo@FreeBSD.org with "unsubscribe freebsd-hackers" in the body of the message