Question(s)

[Michael F. Stemper]

On 24/10/2023 18.15, o1bigtenor wrote:


> What is interesting about this is the absolute certainty that it is impossible
> to program so that that program is provably correct.

Not entirely true. If I was to write a program to calculate Fibonacci
numbers, or echo back user input, that program could be proven correct.
But, there is a huge set of programs for which it is not possible to
prove correctness.

In fact, there is a huge (countably infinite) set of programs for which it
is not even possible to prove that the program will halt.

Somebody already pointed you at a page discussing "The Halting Problem".
You really should read up on this.

> Somehow - - - well - - to me that sounds that programming is illogical.
> 
> If I set up a set of mathematical problems (linked) I can prove that the
> logic structure of my answer is correct.

Exactly the same situation. There are many (again, countably infinite)
mathematical statements where it is not possible to prove that the statement
is either true or false. I want to be clear that this is not the same as
"we haven't figured out how to do it yet." It is a case of "it is mathematically
possible to show that we can't either prove or disprove statement <X>."

Look up Kurt Gödel's work on mathematical incompleteness, and some of the
statements that fall into this category, such as the Continuum Hypothesis
or the Parallel Postulate.

As I said at the beginning, there are a lot of programs that can be
proven correct or incorrect. But, there are a lot more that cannot.

-- 
Michael F. Stemper
Outside of a dog, a book is man's best friend.
Inside of a dog, it's too dark to read.