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
government.
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
English.
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, SlashDot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
