Path: ...!news.mixmin.net!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: Jeff Barnett <jbb@notatt.com>
Newsgroups: comp.lang.lisp
Subject: Re: Lisp history: IF, etc.
Date: Mon, 15 Apr 2024 18:01:46 -0600
Organization: A noiseless patient Spider
Lines: 35
Message-ID: <uvkf5e$iaa5$1@dont-email.me>
References: <uu54la$3su5b$6@dont-email.me> <20240329101248.556@kylheku.com>
 <uu6t9h$dq4d$1@dont-email.me> <20240329104716.777@kylheku.com>
 <uu8p02$uebm$1@dont-email.me> <20240330112105.553@kylheku.com>
 <uudrfg$2cskm$1@dont-email.me> <87r0fp8lab.fsf@tudado.org>
 <uuehdj$2hshe$1@dont-email.me> <87wmpg7gpg.fsf@tudado.org>
 <LISP-20240402085115@ram.dialup.fu-berlin.de>
 <20240402084057.881@kylheku.com> <86h6gjpq3i.fsf_-_@williamsburg.bawden.org>
 <m3frw2vlok.fsf@leonis4.robolove.meer.net>
 <86cyr6pb2l.fsf@williamsburg.bawden.org> <875xwy412p.fsf@nightsong.com>
 <868r1up0wk.fsf@williamsburg.bawden.org> <871q7m3wrj.fsf@nightsong.com>
 <86zfu9ooux.fsf@williamsburg.bawden.org> <87frw03b4j.fsf@nightsong.com>
 <877chbfs00.fsf@yaxenu.org> <87r0f61jkb.fsf@nightsong.com>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Tue, 16 Apr 2024 02:01:50 +0200 (CEST)
Injection-Info: dont-email.me; posting-host="f3d86098fdb1d3f71b0f2237d625750a";
	logging-data="600389"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX1/v+SZquLGHlUjwUAkbbf/AG2OQZJ9rDt8="
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:K7V+fBXCGMT2HSkTq30qSsXEt0E=
In-Reply-To: <87r0f61jkb.fsf@nightsong.com>
Content-Language: en-US
Bytes: 3278

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