[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? :)