5 Aug
2004
5 Aug
'04
12:27 p.m.
>>>> "Paul" == Paul Koning
<pkoning(a)equallogic.com> writes:
>>>> "Steven" == Steven N Hirsch
<shirsch(a)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