Path: ...!weretis.net!feeder8.news.weretis.net!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: David Brown <david.brown@hesbynett.no>
Newsgroups: comp.arch
Subject: Re: Is Intel exceptionally unsuccessful as an architecture designer?
Date: Tue, 8 Oct 2024 09:23:08 +0200
Organization: A noiseless patient Spider
Lines: 45
Message-ID: <ve2mks$23l45$2@dont-email.me>
References: <vcd3ds$3o6ae$2@dont-email.me> <86jzf4829c.fsf@linuxsc.com>
 <vcpojl$2ads5$1@dont-email.me> <vct3av$2tic0$17@dont-email.me>
 <vctb0s$32gol$1@dont-email.me> <vctbo2$32cko$3@dont-email.me>
 <vcv711$3b4hf$1@dont-email.me> <vcvji5$3co45$7@dont-email.me>
 <20240925104320.00007791@yahoo.com> <vdaakm$1facd$4@dont-email.me>
 <vdacqq$1jf40$1@dont-email.me> <vdd6tv$23gqs$1@dont-email.me>
 <vdd8d6$23nsh$1@dont-email.me>
 <ee430ac27c829d5514d5652aa2c6fad6@www.novabbs.org>
 <vdevtm$2c7jg$1@dont-email.me> <vdg6fs$2ko7g$1@dont-email.me>
 <vdh5q8$2pnkp$2@dont-email.me>
 <40853b34aae592d6cd8a19f017e3f7eb@www.novabbs.org>
 <lm2vj6Frf3oU1@mid.individual.net>
 <de251b3b38495a7d423015a83cc842cb@www.novabbs.org>
 <vdis8f$34tqa$2@dont-email.me> <jwvo73vc1e9.fsf-monnier+comp.arch@gnu.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Tue, 08 Oct 2024 09:23:09 +0200 (CEST)
Injection-Info: dont-email.me; posting-host="ba038700c422d685be07d0a9f78a9fd8";
	logging-data="2217093"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX199CGzvjiW280oQS2rB37NVxkHehSG3wLc="
User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:102.0) Gecko/20100101
 Thunderbird/102.11.0
Cancel-Lock: sha1:MJffjW1oTE3+86U6x/gACkZ5x8c=
Content-Language: en-GB
In-Reply-To: <jwvo73vc1e9.fsf-monnier+comp.arch@gnu.org>
Bytes: 4160

On 07/10/2024 18:59, Stefan Monnier wrote:
>> kinds of proofs as "better" than others.  Some dislike "proof by computer",
>> and don't consider the four-colour theorem to be a proven theorem yet.
> 
> "Proof by computer" can mean many different things.  The 1976 proof by
> Appel&Haken failed to convince a number of mathematicians both because
> of the use of a computer and because of the "inelegant", "brute
> force" approach.
> 
> Regarding the use of a computer, it relied on ad-hoc code which used
> brute force to check some large number of subproblems.  For some
> mathematicians, it was basically some opaque piece of code saying "yes",
> with no reason to be confident that the code actually did what the
> authors intended it to do.

Certainly for a "proof by computer" to be acceptable, the software 
involved needs to be considered part of the proof.  It needs to be 
something other mathematicians can read through and agree is correct, 
just like any other bit of the mathematical proof.  Some programming 
languages are more suitable for that task than others - typically you'll 
want something that can handle arbitrary precision integers, automatic 
garbage collection (so that the code is not cluttered with stuff that is 
irrelevant to the real task), and probably a functional programming 
language or style (which is more mathematical in outlook, and easier to 
prove).

And just like you want the "hand-written" maths to be checked by 
multiple mathematicians, computer-based proofs should be confirmed on 
different hardware (so your proof doesn't rely on the Pentium FDIV bug 
or similar), and ideally with the same algorithm re-implemented in more 
than one programming language.  The more redundancy you can get there, 
the more confidence you can have in the results.

> 
> The 2005 proof by Gonthier also used a computer, but the program used
> was a generic proof assistant.  Arguably some "opaque brute force" code
> was used as well, but it generated actual evidence of its claims, which
> was then mechanically checked by the proof assistant.
> 
> That leaves a lot less room for arguing that it's not valid.
> I haven't heard anyone express doubts about that proof yet.
> 
> 
>          Stefan