Question(s)

[Thomas Passin]

On 10/24/2023 7:15 PM, o1bigtenor wrote:
> On Tue, Oct 24, 2023 at 6:09 PM Thomas Passin via Python-list
> <python-list at python.org> wrote:
>>
> snip
>>
>> By now you have read many responses that basically say that you cannot
>> prove that a given program has no errors, even apart from the hardware
>> question.  Even if it could be done, the kind of specification that you
>> would need would in itself be difficult to create, read, and understand,
>> and would be subject to bugs itself.
>>
>> Something less ambitious than a full proof of correctness of an
>> arbitrary program can sometimes be achieved.  The programming team for
>> the Apollo moon mission developed a system which, if you would write
>> your requirements in a certain way, could generate correct C code for them.
>>
>> You won't be doing that.
>>
>> Here I want to point out something else.  You say you are just getting
>> into programming.  You are going to be making many mistakes and errors,
>> and there will be many things about programming you won't understand
>> until you get some good solid experience.  That's not anything to do
>> with you personally, that's just how it will play out.
>>
>> So be prepared to learn from your mistakes and bugs.  They are how you
>> learn the nuts and bolts of the business of programming.
>>
> 
> I am fully expecting to make mistakes (grin!).
> I have a couple trades tickets - - - I've done more than a touch of technical
> learning so mistakes are not scary.
> 
> What is interesting about this is the absolute certainty that it is impossible
> to program so that that program is provably correct.
> 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.

In general, that's not the case - CF Godel's Theorem.  There are true 
arithmetical statements that cannot be proven to be true within the 
axioms of arithmetic.  There's a counterpart in programming called the 
halting problem. Can an arbitrary computer program be proven to ever 
finish - to come to a halt (meaning basically to spit out a computed 
result)?  Not in general.  If it will never halt you can never check its 
computation.

This doesn't mean that no program can ever be proven to halt, nor that 
no program can never be proven correct by formal means.  Will your 
program be one of those?  The answer may never come ...

> That's what I'm looking to do with the programming.
> 
> (Is that different than the question(s) that I've asked - - - dunno.)
> 
> Stimulating interaction for sure (grin!).
>