|Mark Tarver was born too many years ago to count in the
industrial town of Manchester. One of my early memories
include ruined houses still left from the Blitz. I can also
just remember one of the last great smogs (a wonderful
vision, greyish-yellow like catarrh from a smoker's lungs
and thick enough to tap on the window). I wanted to go out
and play in it but was refused. This was my introduction to
the unreasonable world of adults.
My family moved to Jersey where I grew up. I experienced
the Great Freeze of '63 and Hurricane Betsy in '65. I wanted
to go out and play with Betsy too, but guess what happened
to that idea? My school reports showed I did what I wanted
at my own pace and showed little interest in competition.
This was thought of as a problem, although it seems to me to
be precocious wisdom. I followed in the family tradition by
being placed on school probation (my brother was suspended).
Later I changed and the nadir was reached when I went to
I read philosophy at Reading University graduating in 1978
with a first and then going on to Corpus Christi, Oxford.
The college still sends me expensively bound periodicals of
astounding dullness detailing the minutae of college life.
The last one showed a picture of some ancient cloth which I
at first took to be the corroded underwear of Oliver
Cromwell. Expensively bound, pretentious and utterly dull
would well describe Oxford. I took a Ph.D. at Warwick and
found my way into computing by way of the BBC micro.
4 years old in industrial Manchester; with the same
precocious attitude and suave dress sense that I carried
into later life.
I had 32 KB of main memory to play with. It was an
invitation to boldly go where no man has gone before and I was in charge
of the spaceship equivalent of the Galileo shuttle. It was great fun.
From there it was a hop to working in a software company and then to the
philosophy department at Leeds which was investing in computers.
I knew the location of the little red switch at the back on the computer
that turned it on. Who would have thought? Heads were turned. I had
already solved an outstanding open problem and so I got the job. It was
an invitation to mess about for two years with computers.
There was one person in the philosophy department who was treated with
disdain. He smoked continental cigarettes and wore NHS granny glasses
mended with cellotape. His name was Gyorgy and he was a Hungarian in
exile. Gyorgy was unpopular because he actually knew something about
computers and did not hide the fact, and because he wrote impeccably
grammatical English sentences that really required the use of a bracket
balancing editor to read them. One famous example was his seminar
abstract which consisted of a single sentence of 200 words.
Of course Gyorgy wrote in Lisp and so I was hooked. We competed for the
attentions of the DEC-10 mainframe, a class act who bestowed her favours
impartially on both admirers. Gyorgy was infamous in computer support
for resource-hungry Lisp programs that dimmed the lights whenever he ran
They were good times and of course they could not last. The government
got wind of the fact that we weren't actually producing anything, but
enjoying ourselves and put a stop to it. After two years of anarchy with
Lisp, in 1988 I was sent to the LFCS in Edinburgh for correctional
training in ML. Two years after that I returned to Leeds and gave my
talk on ML. The first slide was titled
Why is Programming in ML like Safe Sex?
Because you can't catch any bugs but it's not much fun.
But I liked the idea of pattern-matching and borrowed this
for Lisp. Thus was taken the first step to Shen.
Leeds was fun at first and then it too got very serious. The department
took the government directives seriously and started to turn itself into
a 'centre of excellence'. Finding myself increasingly out of step with
the fuhrer directives, I left in 1999.
Then off to America in 2002 and Stony Brook. I was an instructor for
discrete maths and given a deadly book by a chap called Anderson as the
course text. Weighing the equivalent of bucket of lard and about as
digestable, it turned me off so much that I donated it to a grad student
and rewrote the course. We used computer-assisted proof to learn logic
and these innovations seriously annoyed the UG committee. My resignation
was a foregone conclusion but still remains, in my view, a masterpiece
of how to napalm your bridges in style. It also contains a plea for
making computer science coherent and interesting. From the ashes of that
course was to spring Logic, Proof and Computation.
At 56 what I've learnt from life is that if you want to be free, you
have to work at it and make sacrifices. Most particularly you have to
beware people who tell you that true freedom is giving them your work
and time for free. Remember if you're not irritating somebody, you're
not being yourself.