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@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!).
--
https://mail.python.org/mailman/listinfo/python-list
