Re: Lisp history: IF, etc.

On 4/15/2024 2:01 PM, Paul Rubin wrote:

Julieta Shem <jshem@yaxenu.org> writes:

I also agree that he was a logician: he worked on a mathematical basis
for computer science.  A mathematical basis for computer science must be
classified as logic.

 Mathematical logic is an area that deals with topics like proof theory.
Not to diminish McCarthy in any way, but it sounds like he didn't work
in that particular area.

Well he and a PhD student (named not recalled) developed a compiler for a Lisp that was of about the complexity of a mid 1960s Lisp. Then they formally proved that the compiler was correct. This was NOT "proof theory" as you probably meant it in the above paragraph. However in my my mind the hairiest problems with the venture were setting up the mechanisms and criteria for representing the code and expected behavior plus enumerating the proof rules. A good deal of theory was developed and buried in their effort.
I also remember McCarthy in the late 1960s being obsessed with logic and philosophy and randomly spouting off discussions such as how processing of
    Sir Walter Raleigh was the author of "The Lie"
    Did the Queen know that Raleigh wrote "The Lie"?
might produce
    Did the Queen know TRUE?
I heard him bring up such questions many times because he was hoping that logical calculi could support natural language processing and reasoning. The above was offered as an example of a problem at the relatively simple surface level.
--
Jeff Barnett