[kazinator]

If every operation can have any type arguments applied to it and does something sensible with no compiler or run-time error ... good luck debugging, surely.

What happens with OOP? Every class has to understand how to "bark", not only the dog class?

If any class can somehow "bark" without throwing an exception, that may not be in alignment with the programmer's intent, or promote the furtherance of his or her goals in any way.

For intance, the intent may be that the programmer wanted to ask the local variable dog to "bark", but misspelled it as ndog and the integer which counts the number of dogs was asked to bark instead.

There is much value in identifying the problem that an integer doesn't bark.

[Animats]

Boyer-Moore theory has "shells", which are like structures. See page 39 of [1]. Since this is a pure functional language, values cannot be altered. Shells have constructors, a type predicate, and can have restriction predicates on values.

    Shell Definition.
    Add the shell ADD1 of one argument
    with bottom object (ZERO),
    recognizer NUMBERP,
    accessor SUB1,
    type restriction (NUMBERP X1),
    default value (ZERO), and
    well-founded relation SUB1P.

It's not intended that you run programs in Boyer-Moore theory, although you can. It's a proof tool.

[1] https://www.cs.utexas.edu/users/boyer/acl.pdf

[kazinator]

I will have to read this to understand what we can prove with this; or rather, what kinds of wrongs in a program under this theory are usefully proved to be false.

---

Ouch; did you see that "overfull hbox" that got rendered out in the first line of paragraph 3 of the Preface? :)