This is a bit of input to Ken Kubota's research, which has resulted in
on his nice little genealogical diagram as "by Roger Jones", due to a
bit of overgenerous
credit given by Rob Arthan.
Rob and I usually describe each other in this kind of context as
"co-architects" of ProofPower,
which is a pretty weak characterisation of our relationship and
contributions, but saves
boring all with too much detail, which I am now going to do.
The story of ProofPower begins in 1986 when I was asked by Roger Stokes
at ICL to join a
new team set up to apply formal methods to the design and verification
of highly secure
GCHQ/CESG had by then already decided that they wanted their contractors
with the Z specification language and Roger Stokes was looking at
Boyer-Moore and HOL
as possible tools to use for reasoning about Z specifications.
I pretty quickly decided that HOL was the better bet and set about
making that work,
initially using manual transcriptions from Z into HOL.
A couple of years later I had been put in charge of the "High Assurance"
an opportunity arose to undertake a collaborative R&D project
part-funded by the UK
I recommended that we put together a project under which ICL could
develop a proof
tool for Z working by semantic embedding of Z into HOL, and that to
provide a stable
basis for this work which would underpin the future business of the team
do a new implementation of a HOL proof tool.
This eventually was called "ProofPower" (primarily for marketing
reasons, ICL then had
several products with names ending in "Power" of which the most
important was OfficePower).
So I put together a collaboration which included Cambridge University
(actually the maths department doing some logical theory), Kent
University (Keith Hanna)
and Program Validation Limited (a Southampton University spin-off with a
set of tools
for static analysis and verification of programs in the SPARK subset of
The idea to include the CU maths department was Mike Gordon's who was
ICL as a consultant for the duration of the project, even though the
Labs did not have a formal involvement.
So ProofPower was by baby, it was my idea, I put together the project,
bid for the funding
and most importantly, knowing that a full-time team leader was needed
and that I could
not devote all my time to it, I invited Rob Arthan to join us and lead
In terms of contributions to that first project, Rob was the main force.
I did not contribute a single line of code, but I was involved in all
the design reviews
that took place and some of the original features of the ProofPower
were suggested by me.
My most substantial technical contribution was probably the design of
the Z embedding,
working out how the derived rules for reasoning with Z would work, and
in some of the
changes to the inference rules, tactics, and goal package which made the
to the characteristics of the embedded language, and made it possible to
reason in Z
without necessarily having to understand the mapping into HOL.
(ProofPower was designed from the start to support logical pluralism via
That's just about the original 3-year project which created ProofPower,
in the subsequent history
my own involvement has been very small.
If any single person should have the ProofPower by-line, then it should
certainly be Rob,
but I naturally prefer Arthan/Jones or some other joint attribution,
because I still think
of ProofPower as "my baby", in contexts where the entire team cannot be
But this isn't one of them so here, for the record is the list of
Roger Bishop Jones
My biggest regret is the divergence of ProofPower from the rest of the
though I don't know how we could then have prevented that from happening.
"Open-source" was a pretty new idea then, particularly as far as
industry was concerned.
Credit for the Simple Theory of Types
Ken's diagram makes it look like this theory begins with Church.
Its not entirely uncontroversial as to who should have credit for
devising this system.
Most frequently credit has been given to Ramsey, but though he seems to
have had the
idea pretty early on, he never formulated the logical system in detail
(and one might think
that the idea of simplifying Russell's ramified theory would have
occurred to others).
Recent scholarship suggests that the first fully detailed account of STT
as a formal
system is due to Rudolf Carnap, who, in the course of writing a
to facilitate the application of formal logic in mathematics and
science, decided to
base it around the simplified rather than the ramified type theory.
I think this particular formulation may have escaped attention because
"Abriss der Logistik" was written in German and has never been
Until recently the more widely know text by Hilbert and Ackermann was
to be the first formal account of the simple theory of types.
STT appears I believe, only in the second edition of their text, so
first edition (1928) precedes Carnap's (1929) text, he still was in
first with STT.
There were many later textbooks which presented this version of STT
(not based on the lambda-calculus and having "power set" as the primitive
type constructor), which was probably the dominant conception of STT
(and may still be, among logicians) until Mike Gordon adopted
and adapted Church's version for HOL.
So maybe a little circle with "(Ramsey/Carnap)" at the top of the STT box?
I wondered what the significance of the shape of boxes in the diagram was.
It looked like most of the rectangles were proof tools and the elipses
were theories, but that seems not quite consistent.
Check out the vibrant tech community on one of the world's most
engaging tech sites, SlashDot.org! http://sdm.link/slashdot
hol-info mailing list