[Prev][Next][Index]
Dismay
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
Larch.
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
select(insert(e,s))==e.)
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
asserts
\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