On 01/02/2023 08:07, Aharon Robbins wrote:> I've never understood this.
Isn't there a chicken and egg problem?
> How do we know that the theorem prover is correct and bug free?
A theorem prover generates a proof of the theorem (if it succeeds).
Checking the correctness of a proof is a much simpler task
than finding the proof in the first place and can be carried
out independently by different teams using different methods.
Appel and Haken's proof of the four colour theorem, for example,
involved a significant element of computer checking which was
independently double checked with different programs and computers.

> [It's a perfectly reasonable question. Alan Perlis, who was my thesis
> advisor, never saw any reason to believe that a thousand line proof
> was any more likely to be bug-free than a thousand line program.
> -John]

Mathematicians publish proofs all the time and only a tiny percentage
of published proofs turn out to have errors. Programmers release
programs all the time and a vanishingly small percentage of these
turn out to be free from all bugs. Alan Perlis may not have been able
to think of a reason why this should be the case, but it is,
nevetheless, the case.

--
Martin

Dr Martin Ward | Email: martin@gkc.org.uk | http://www.gkc.org.uk
G.K.Chesterton site: http://www.gkc.org.uk/gkc | Erdos number: 4
[Computer programs tend to be a lot longer than mathematical proofs. I
realize there are some 500 page proofs, but there are a whole lot of
500 page programs. It is my impression that in proofs, as in progams,
the longer and more complicated they are, the more likely they are to
have bugs. -John]

Dr. Ward replied to me privately also, but since this went to the group,
I'll say the same thing here that I replied to him.

In article <23-02-005@comp.compilers>, Martin Ward <martin@gkc.org.uk> wrote:
>On 01/02/2023 08:07, Aharon Robbins wrote:
>> I've never understood this. Isn't there a chicken and egg problem?
>> How do we know that the theorem prover is correct and bug free?

>A theorem prover generates a proof of the theorem (if it succeeds).
>Checking the correctness of a proof is a much simpler task
>than finding the proof in the first place and can be carried
>out independently by different teams using different methods.
>Appel and Haken's proof of the four colour theorem, for example,
>involved a significant element of computer checking which was
>independently double checked with different programs and computers.

This tells me what a theorem prover does, and why it's useful. It
does not answer my question: How do we know that the theorem prover
itself is correct and bug free?

>> [It's a perfectly reasonable question. Alan Perlis, who was my thesis
>> advisor, never saw any reason to believe that a thousand line proof
>> was any more likely to be bug-free than a thousand line program.
>> -John]

And this is a different point from my question.

>Mathematicians publish proofs all the time and only a tiny percentage
>of published proofs turn out to have errors. Programmers release
>programs all the time and a vanishingly small percentage of these
>turn out to be free from all bugs. Alan Perlis may not have been able
>to think of a reason why this should be the case, but it is,
>nevetheless, the case.

I don't argue this. But I think mathematical theorems and their
proofs are different qualitatively from real world large programs.
I do think there's room for mathematical techniques to help
improve software development, but I don't see that done down
in the trenches, and I've been down in the trenches for close
to 40 years.

Arnold
--
Aharon (Arnold) Robbins arnold AT skeeve DOT com

Martin Ward <mwardgkc@gmail.com> writes:
>On 01/02/2023 08:07, Aharon Robbins wrote:> I've never understood this.
>> [It's a perfectly reasonable question. Alan Perlis, who was my thesis
>> advisor, never saw any reason to believe that a thousand line proof
>> was any more likely to be bug-free than a thousand line program.
>> -John]
>
>Mathematicians publish proofs all the time and only a tiny percentage
>of published proofs turn out to have errors.

Even at face value I would like to see some evidence for this claim.

A comparable statement would be "Computer scientists publish papers
about programs all the time, and only a tiny percentage of these
papers turn out to have errors".

There is a difference between how a mathematical proof is used and how
a program is used.

1) A program is usually fed to a machine for execution. A published
proof is read by a number (>=0) of mathematicians, who fill in a lot
of what the author has left out. If you feed the published proof to
an automatic proof checker (of your choice), how many of the published
proofs need no additions and no changes (bug fixes) before the proof
checker verifies the proof. I guess there is a reason why Wikipedia
has no page on "proof checker", but suggests "proof assistant": "a
software tool to assist with the development of formal proofs by
human-machine collaboration."

2) A program has to satisfy the requirements of its users, while a
published proof is limited to proving a published theorem. One
example of the difference is that undefinedness is totally acceptable
in mathematics, while it is a bug in programs (interestingly, there is
a significant number of compiler writers who take the mathematical
view in what they provide to programmers, but consider that a program
in their programming language that exercises the undefined behaviour
that they provide to programmers to be buggy).

The size argument that our esteemed moderator provided also has to be
considered.

- anton
--
M. Anton Ertl
anton@mips.complang.tuwien.ac.at
http://www.complang.tuwien.ac.at/anton/

On Sun, 05 Feb 2023 17:59:03 GMT
anton@mips.complang.tuwien.ac.at (Anton Ertl) wrote:
> 2) A program has to satisfy the requirements of its users, while a
> published proof is limited to proving a published theorem. One
> example of the difference is that undefinedness is totally acceptable
> in mathematics, while it is a bug in programs

All programmes have de facto limitations in the input they can process
correctly imposed by the hardware , operating system , etc. If they advertise
that they will detect some kind of invalid input and fail to do so , that's a
bug. If they make no such claims then it boils down to whether one can
"reasonably" expect the programme to detect the invalid input and report it but
what counts as reasonable will generally be a matter of dispute. Note also
that there can be grey areas. For example a numerical analysis programme may
produce for some range of inputs an output which is not 100% correct but
"close enough". But what's close enough depends on many factors.

> (interestingly, there is
> a significant number of compiler writers who take the mathematical
> view in what they provide to programmers, but consider that a program
> in their programming language that exercises the undefined behaviour
> that they provide to programmers to be buggy).

This is a cryptic comment. To the extent that I can guess from knowing
about your pet peeves what you're talking about , I don't think what
you say describes the views of compiler writers.