You should not expect a TLA+ specification of a program to be shorter
than the program. Programming languages are designed to write
programs. There's no reason a TLA+ spec that captures the meaning of
a program should be as short as the program itself. For example, the
program might have an assignment statement x = x+1 . The TLA+ formula
x' = x+1 may look similar, but it's not at all the same. For one
thing, the statement x = x+1 is supposed to throw an exception if x
is too large. So, its TLA+ representation would have to be something
like
IF x+1 =< MaxInt THEN x' = x+1 ELSE ...
plus a whole lot of additional math representing the actions that
describe exception handling. On the other hand, how would you express
the TLA+ formula x' = x+1 in the programming language? Program code
to add two arbitrary integers is not going to be simple. (Of
course it won't be difficult if someone has aleady implemented it; but
a TLA+ spec that someone has already written isn't hard to import
either.)
Programming languages make it easy to handle the complexities of
arithmetic on a finite set of integers, and hard to do simple
arithmetic on the actual set of integers. It's obvious why
programming language designers made that choice. It's less obvious
why I made the opposite choice for TLA+, and most people don't
understand it. To get a hint of the reason why TLA+ is so different
from programming languages, read the story of the OpenComRTOS project
described here:
Experienced programmers don't get a factor of 10 reduction in code
size by improving their programming; they do it by changing the way
they think. Learning to think in terms of algorithms and high-level
concepts rather than programs and code takes time and practice. I
learned to do it before I became a computer scientist, but it took me
25 years to figure out how to embody that kind of thinking in a
specification language. Don't expect to learn it in a few days.
Leslie