My first experience of programming was working on a Burroughs mainframe while employed by the GEC in 1979 on the System X project. System X marked the transition of phone networks from electromechanical relays to digital technology. This experience didn't really leave much impression on me, and I picked up the trail more definitively in 1984, when my father brought home from school, the BBC model B mcrocomputer.

This was a revelation to me, as it was for so many others, and I wrote my first programs in BBC Basic. I graduated from there to working for a software company using the language DBase II; a 4th generation database programming language bought up by Ashton-Tate and derived from an earlier language called Vulcan. After a time I noticed that the programs I was writing seemed rather similar, and that therefore I could get the computer to write them for me. This is an example of my precocious interest in metaprograms, programs that write programs, that was to remain with me throughout my career.

Move to Academia

I moved from commercial programming into academia in 1986 and into AI in the form of a natural language project into speech act theory. There I picked up two interests; the representation of natural languages to the computer and automated reasoning. I quickly moved to Common Lisp, the premiere language for metaprogramming, and started writing metaprograms. The first metaprogram I wrote, when at the LFCS in Edinburgh, compiled an untyped pattern-matching functional language somewhat in the style of ML into Lisp. The second program followed the architecture of Stickel's Prolog Technology Theorem Prover into compiling first-order theories into code. This involved building a Prolog compiler in Lisp. I had actually discovered the key ideas of Stickel's work for myself before I came across his work.

First Prototype: SEQUEL

In 1993 I published a paper, A Language for Implementing Arbitrary Logics, in AAAI. This language, SEQUEL (SEQUEnt processing Language) brought together the diverse elements of my interests. SEQUEL added types to my untyped language and the types were specified in sequent calculus rules and, using my Prolog compiler, the rules compiled to effect type checking. From 1993-2005, SEQUEL went through a series of refinements that slimmed it down and made it conceptually less dependent on Lisp. The typechecking algorithm was improved and so was the Prolog compiler technology.

Second Prototype: Qi

The resulting language Qi, was released in 2005. Qi was about 30X faster than SEQUEL at verifying type security and 4X smaller in the code base (6,000 lines vs 23,000 lines). The latter was gained by conceptually distancing Qi from Common Lisp and avoiding the attempt to specify the type theory of the underyling Lisp. In 2008, I published Functional Programming in Qi. This work contained a semantics and a correctness proof of the Qi type system.

Second Prototype: Shen

In 2009 I was an invited speaker to a Lisp conference, where I suggested that Qi could be totally separated from Common Lisp. Common Lisp was huge, and I believed that Qi could be specified in a Lisp-like language that was much smaller. In the place of the 700+ system functions in Common Lisp, I estimated that the new language could be specified in less than 50. This Lisp like language, which became known as Kλ would function as a virtual machine for compiling the new version of Qi. By simply implementing a Kλ compiler in a language, you could then move Qi to that language. The new version was to be Shen, which appeared in 2011.

Shen improved on Qi. During my time at Leeds, from 1986 to 1988 and again from 1990 to 1999, I was exposed to Gyorgy Lajos' Ph.D. work on MetaLisp. MetaLisp was a compiler-complier written in Lisp, and designed to implement a general programming approach that Gyorgy called language directed programming. I later reimplemented MetaLisp as a component of Shen (Shen-YACC), but not as a general purpose language to replace Shen, but to encode the compilers that were part of the Shen kernel. Both Shen-YACC and the Prolog compiler are left exposed for the user as part of the Shen environment. In 2021, Shen was rewritten for style and conciseness, making it even easier to port, and the facility for type checking Shen-YACC was added. The entire program is now only 4,000 lines.

Shen is entirely written in Shen; there is no specifically Lisp code left in it. This meant it could be ported to any language and Shen has been ported to 14 different languages by programmers around the world.

Stuff to Read

The above history is recorded in more detail online here. The website for Shen contains over 1,200 web pages, but the place to head to is the learning page which details all the online materials. The canonical reference is the Book of Shen, fifth edition. This is a tome, and is fairly dense in places. The 4th edition, which is still fairly relevant, can be read online. You can download Shen from the Shen website.