This is mostly a cry of dismay, accompanied by one positive
suggestion.  In the last several months, I've refereed (and encouraged
rejection of) a few papers about applications of Larch.  Virtually
every non-trivial trait included in this small and non-random sample
was inconsistent.  In some cases that can be blamed on insufficient
knowledge of mathematics; in others, on insufficient knowledge of

The commonest "purely mathematical" mistakes occurred in definitions
by recursion -- such as the ever-popular ill-defined recursion over
constructors that don't freely generate a sort.  (You know the kind of
thing: defining the operation select:Set->Element by the axiom

The commonest confusion about Larch can be illustrated by the
following made up example: The user wants to define a sort of
"non-atomic events", characterized by a starting time and a finishing
time, both measured in integral clock ticks, and with the finish
guaranteed to be later than the start, so he says

    NonAtomic : trait
       Event tuple of start : Int, stop Int
       \forall e: Event
          e.start < e.stop

The positive suggestion is that Larch pedagogy make a point of
warning against this.

The experience has made me more sympathetic to formalisms that
include some form of "definitional principle" (e.g., HOL, PVS, the
various versions of Boyer-Moore, ...) guaranteeing the consistency of
the theories introduced.

- David Guaspari