Date: Wed, 9 Oct 2002 14:59:01 -0700 From: Ted Faber <faber@ISI.EDU> To: Terry Lambert <tlambert2@mindspring.com> Cc: "Nelson, Trent ." <tnelson@switch.com>, "'hackers@freebsd.org'" <hackers@freebsd.org>, "'questions@freebsd.org'" <questions@freebsd.org> Subject: Re: FreeBSD usage in safety-critical environments Message-ID: <20021009215900.GC93282@pun.isi.edu> In-Reply-To: <3DA482D6.F618F6C5@mindspring.com> References: <8F329FEDF58BD411BE5200508B10DA7607D71A10@exchptc1.switch.com> <3DA482D6.F618F6C5@mindspring.com>
next in thread | previous in thread | raw e-mail | index | archive | help
--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
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?20021009215900.GC93282>