Luxasm news


Message: 1
Date: Tue, 3 May 2005 13:24:35 +0100 (BST)
From: "C.R. Chafer" <co.uk>
Subject: Re: [Luxasm-devel] Re: +AFs-Luxasm-devel+AF0- Re: RosAsm is a broken pile of crap

--- Johannes Kroll <x.de> wrote: 
On Sun, 1 May 2005 11:08:12 +0100
"Beth" <BethShot.com> wrote:


> It's all possible: From "screw it, who cares?" and the unsaved
> work is just lost (which is, in fact, the usual practice of 99%
> of programs, whether you think that's a sensible choice or
> not)...all the way to getting so paranoid with the package as
> to make it "virtually uncrashable" and apply full "formal"
> design and verification to the levels used for nuclear
> powerplants, space shuttles and so forth (but note that this
> latter option is _immensely difficult and time-consuming_...

This will just never work... 

Oh it can; just, as Beth says, it is a real pain and hence
not justified for a programme of the size of Luxasm.

I have done a restricted version of this before on a piece of
code I developed a year or so ago, though I only did a partial
mathematical proof (I'd have to read-up on how to go about doing
a full proof), checking every line for all possible errors took
nearly a week for only a few hundred lines of code.  (The code
was for the scheduler and major components of the core of the
kernel of the OS I've been developing on-and-off for years, so
spending the time making things perfect was justified in that
case.)

Never-the-less it would be a good idea to verify the code
matches the design _after_ it has been written, starting with
the major components (such as error recovery), if for no other
purpose than writing a section of the documentation on how to
do this with Luxasm.  That is for the future though.

C
2005-05-03
.