Skip site navigation (1)Skip section navigation (2)
Date:      Tue, 11 Jan 2011 17:05:38 -0500
From:      Lowell Gilbert <freebsd-current-local@be-well.ilk.org>
To:        Boris Kochergin <spawk@acm.poly.edu>
Cc:        David DEMELIER <demelier.david@gmail.com>, freebsd-current@freebsd.org, freebsd-chat@freebsd.org
Subject:   Re: why panic(9) ?
Message-ID:  <444o9fhz9p.fsf@be-well.ilk.org>
In-Reply-To: <4D2CC06A.8080408@acm.poly.edu> (Boris Kochergin's message of "Tue, 11 Jan 2011 15:41:14 -0500")
References:  <AANLkTi=OQbS-0jJx0YwZhM7xDWPLOkaYYZAYfESUEvvM@mail.gmail.com> <4D2CC06A.8080408@acm.poly.edu>

next in thread | previous in thread | raw e-mail | index | archive | help
[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.  



Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?444o9fhz9p.fsf>