[Oberon] Re. "rock solid"/reliable software:
lab.eas at gmail.com
Thu Nov 6 19:04:02 CET 2014
Ada had that declared aim. Is it still alive?
Wirth advocated simplicity; if the whole-picture is small enoungh,
you can *see* the faults. But few tasks can be kept small enoungh.
Eiffel introduced checking mechanisms beyond strict typing, but nobody
There's been talk/research about formal methods: where you could "prove
the results, via algebraic manipulation of the code". Or better still have the
computer auto-prove the code.
Searching the literature in this direction I came across repeated claims
that certain functional languages could formally prove correctness via
algebraic manipulation of the code. Several examples of manipulating
the code of the language: joy; were published, but I never saw a complete
task being proved.
It seems like the Artificial Intelligence wave of the 70's: they eventually
settled for expert-systems, which works more like a horse-and-rider.
I.e. the user and system collaborate. Which is where ETHO has been for
What did we call those low-flying-missiles, which automatically found
their targets, and have now been replaced by horse-and-rider drones?
== Chris Glur.
More information about the Oberon