Hardware/doc preservatoion, was Re: rarest computers.

From: Dwight K. Elvey <dwight.elvey_at_amd.com>
Date: Thu Aug 5 20:00:43 2004

>From: "Paul Koning" <pkoning_at_equallogic.com>
>
>>>>>> "Paul" == Paul Koning <pkoning_at_equallogic.com> writes:
>
>>>>>> "Steven" == Steven N Hirsch <shirsch_at_adelphia.net> writes:
> Steven> On Wed, 4 Aug 2004, ben franchuk wrote:
> >>> PS. Years ago in BYTE ( early 1990's? ) they had spoke up of a
> >>> CPU designed for reliable operation for real time control of
> >>> things like power plants or subways or aircraft. They claimed it
> >>> was so simple that programs could be proven to be bug free. I was
> >>> wondering if they manufactured or sold any the devices.
>
> Steven> That would be the British "Viper" CPU. Computational theory
> Steven> suggests (proves, perhaps? - it's been a few years) that use
> Steven> of hardware or software stacks renders behavior
> Steven> indeterminate.
>
> Paul> Baloney. Anyone who has paid any attention to Dijkstra knows
> Paul> that such a statement would have to be complete and utter
> Paul> nonsense.
>
>PS. It is certainly true that programs can be proven to match their
>specification. That's not quite the same as proving them bug free --
>it now requires the specification to be bug free.
>
>But such proofs in no way require the absence of a stack. That's
>actually rather obvious, because any program that uses a stack can be
>rewritten into a program that does not use one. But in fact such a
>rewrite does not help readability at all.
>
>It probably is not a coincidence that the scientist who did much early
>work on stacks is also the scientist who spent a lifetime working on
>program correctness (E.W.Dijkstra).
>
> paul
>

Hi
 I think that it is interesting that there is a programmer
in the UK that produces one of the few provable program
products for correctness ( to specification ) that meet
some standard ( I forget which ) and his programs are all
done in Forth ( that uses two stacks ).
 My understanding is that most of the reason he can produce
this is that the language it self is built and verified
by him and that even though there are stacks, use is
usually more controlled and maximum depths can be calculated.
Most Forth processes are done with cooperative tasking rather
than the more random effects of preemptive. This also means
better predictability.
 The other part is that Forth programs tend to be highly
factored. This means that hierarchical verification is
more practical. It is easier to understand the range
of valid inputs for each piece and how those effect the
next level up.
 He writes program for such things as subway control systems.
His products need to meet tight controls that need to be
absolutely correct or people die. Strange that he would
use a language that not only uses a stack but uses two stacks
and still produces verifiable results. He considers that
choice to be a most important one.
Dwight
Received on Thu Aug 05 2004 - 20:00:43 BST