Questions on proof assistants

[Lawrence Paulson]

> On 15 May 2020, at 11:54, Freek Wiedijk <freek at cs.ru.nl> wrote:
> 
> - Isabelle imported a lot of analysis from HOL Light.
>  The original formalization was written by John Harrison,
>  and the conversion was done by Larry Paulson.  I _don't_
>  think this was automatic, I think Larry just "ported"
>  the proofs manually by replaying John's proofs and then
>  mimicking that in Isabelle.

Well, I wanted to grab all the useful material. It’s fortunate that I was familiar with HOL Light’s tactical language, having designed much of it myself in 1984. I was able to port most of the proofs without the bother of actually running HOL Light (you have to build it from sources every time, and loading the libraries takes hours, bah). I used a shell script to assist in the conversion, but the rest of the work was manual. Part of my aim was to make my own scripts clear enough that the next person would not have to work so hard.

Often I didn’t have the faintest idea what I was porting; for example, please don’t ask me what a homology is (or what it is for); I was able to port the HOL Light homology library without picking up any useful knowledge. This is what makes me believe that a high level, source-to-source translation process will become feasible. It’s much more desirable than low-level proof translations, which yield not proofs but merely assertions of the form “computer says it’s a theorem”.

Larry