From owner-freebsd-chat@FreeBSD.ORG  Tue Jan 11 22:32:19 2011
Return-Path: <owner-freebsd-chat@FreeBSD.ORG>
Delivered-To: freebsd-chat@freebsd.org
Received: from mx1.freebsd.org (mx1.freebsd.org [IPv6:2001:4f8:fff6::34])
	by hub.freebsd.org (Postfix) with ESMTP id 84094106564A
	for <freebsd-chat@freebsd.org>; Tue, 11 Jan 2011 22:32:19 +0000 (UTC)
	(envelope-from freebsd-current-local@be-well.ilk.org)
Received: from mail3.sea5.speakeasy.net (mail3.sea5.speakeasy.net
	[69.17.117.42]) by mx1.freebsd.org (Postfix) with ESMTP id 5D00A8FC08
	for <freebsd-chat@freebsd.org>; Tue, 11 Jan 2011 22:32:19 +0000 (UTC)
Received: (qmail 16701 invoked from network); 11 Jan 2011 22:05:39 -0000
Received: from dsl092-078-145.bos1.dsl.speakeasy.net (HELO be-well.ilk.org)
	([66.92.78.145])
	(envelope-sender <freebsd-current-local@be-well.ilk.org>)
	by mail3.sea5.speakeasy.net (qmail-ldap-1.03) with SMTP
	for <spawk@acm.poly.edu>; 11 Jan 2011 22:05:39 -0000
Received: by be-well.ilk.org (Postfix, from userid 1147)
	id A19C050825; Tue, 11 Jan 2011 17:05:38 -0500 (EST)
From: Lowell Gilbert <freebsd-current-local@be-well.ilk.org>
To: Boris Kochergin <spawk@acm.poly.edu>
References: <AANLkTi=OQbS-0jJx0YwZhM7xDWPLOkaYYZAYfESUEvvM@mail.gmail.com>
	<4D2CC06A.8080408@acm.poly.edu>
Date: Tue, 11 Jan 2011 17:05:38 -0500
In-Reply-To: <4D2CC06A.8080408@acm.poly.edu> (Boris Kochergin's message of
	"Tue, 11 Jan 2011 15:41:14 -0500")
Message-ID: <444o9fhz9p.fsf@be-well.ilk.org>
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/23.2 (berkeley-unix)
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Cc: David DEMELIER <demelier.david@gmail.com>, freebsd-current@freebsd.org,
	freebsd-chat@freebsd.org
Subject: Re: why panic(9) ?
X-BeenThere: freebsd-chat@freebsd.org
X-Mailman-Version: 2.1.5
Precedence: list
Reply-To: freebsd-chat@freebsd.org
List-Id: Non technical items related to the community
	<freebsd-chat.freebsd.org>
List-Unsubscribe: <http://lists.freebsd.org/mailman/listinfo/freebsd-chat>,
	<mailto:freebsd-chat-request@freebsd.org?subject=unsubscribe>
List-Archive: <http://lists.freebsd.org/pipermail/freebsd-chat>
List-Post: <mailto:freebsd-chat@freebsd.org>
List-Help: <mailto:freebsd-chat-request@freebsd.org?subject=help>
List-Subscribe: <http://lists.freebsd.org/mailman/listinfo/freebsd-chat>,
	<mailto:freebsd-chat-request@freebsd.org?subject=subscribe>
X-List-Received-Date: Tue, 11 Jan 2011 22:32:19 -0000

[Replies redirected.]

Boris Kochergin <spawk@acm.poly.edu> writes:

> All modern operating systems? Maybe some niche ones, like the ones
> that run on Mars rovers, have made progress towards formal
> verification and are believed not to crash given correctly-functioning
> hardware.

The Mars rovers run on VxWorks.  Which is a system I like, but it
isn't anything like formally verifiable.  And it certainly does the
equivalent of FreeBSD panic() under some circumstances.