[Oberon] Re. "rock solid"/reliable software:

[eas lab]

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
  seemed interested.

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
decades.

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.