This is a bit of input to Ken Kubota's research, which has resulted in ProofPower appearing 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
computer systems.
GCHQ/CESG had by then already decided that they wanted their contractors to work 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" team, and 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 we would
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 Ada
programming language).
The idea to include the CU maths department was Mike Gordon's who was engaged by ICL as a consultant for the duration of the project, even though the Cambridge Computer
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 the team.

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 implementation
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 system sensitive 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 semantic embedding).

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 credited.

But this isn't one of them so here, for the record is the list of contributors:

Mark Adams
Rob Arthan
Kevin Blackburn
Phil Clayton
Adrian Hammon
Adrian Hayward
Roger Bishop Jones
Dave King
Gill Prout
Geoff Scullard
Roger Stokes
Piotr Trojanek

My biggest regret is the divergence of ProofPower from the rest of the HOL community,
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 logistics textbook 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 the book "Abriss der Logistik" was written in German and has never been translated into
Until recently the more widely know text by Hilbert and Ackermann was thought
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 though the 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.

Roger Jones

Check out the vibrant tech community on one of the world's most 
engaging tech sites,!
hol-info mailing list

Reply via email to