Ron's post raises two questions. The first is, do we need to specify
programs in a higher-level language before implementing them in a
programming language? People who design PLs would say no, their
languages make what the program does so obvious that no higher-level
description is needed. I think the first PL for which this was
believed to be true was FORTRAN. It's not true for FORTRAN and I don't
think it's true for any existing general-purpose PL--certainly not
when it comes to implementing distributed systems.
It would be nice if there were a PL that made higher-level specs
unnecessary. I think many people working on Milner concurrency have
that as their goal. I believe it would be possible to compile TLA+
specs that use a specific way of describing interprocess communication
into adequate code for a useful class of distributed programming
problems. Testing that belief would be an interesting research
project. I believe that if specs separate from programs are ever made
completely unnecessary, it will not be by PL development. Rather, it
will come through advances in machine learning that allow code to be
generated from something that looks more like a TLA+ spec than like a
program in any currently envisioned language. But that is pure
speculation, and should not be taken seriously.
The current need for specs as well as programs raises the second
question: should those specs look as much as possible like programs to
make them easier for computer engineers to write? I think most
engineers would answer yes. I say no. I think the most important
function of writing a spec is to make the engineer think clearly about
what she is building. I have found conventional programming languages
to be impediments to clear thinking. TLA formalizes the way I learned
over many years to think about concurrent algorithms--the heart of
Dijkstra concurrency. I developed TLA+ to be a language that forces
engineers to think that way about their concurrent systems, rather
than the way PLs lead them to think.
I have given my answers to these two questions, but I don't have time
to justify them properly. I would be interested in knowing how
engineers who have used TLA+ in building distributed systems answer
them, and why.
Leslie