Hi Ernie,
As expected, we are having an agreement. Just a couple of remarks.
I've generally failed in my efforts to get engineers to write down
refinement maps (or even document serialization points in their code),
but armed with the TLC carrot, you have perhaps had better success.
Engineers in industry have told me that they were interested in
checking implementation of a higher-level spec, but I don't know if
any of them have ever done it. They generally check invariants and
perhaps simple liveness properties.
Many interesting protocol specifications don't require existential
quantifiers... This is the sense in which I was saying that TP really
is a step up from what many (most?) engineers do with TLC.
I'd probably characterize those "interesting protocol specifications"
as high-level designs from which people code. TP is a step up because
it's an abstract spec of what a system is supposed to do rather than a
design. The only other industrial examples of abstract specs I know
about have been weak memory models. They have been specified
axiomatically rather than with a real state machine as in a classic
TLA+ spec, so no one really understands them. (Example: We once wrote
a TLA+ spec of the Itanium memory model that just added a variable to
capture the complete history and trivially built the axioms into the
state machine. Using it, model checking discovered errors in some of the
examples in Intel's document describing the Itanium memory.) I haven't heard
of anyone actually verifying that a chip design implements such a weak
memory model. Engineers I knew just checked some consistency
requirements specified as invariants.
Leslie