Whoa!

The question cannot be about whether it is possible to prove any abstract program will be correct and especially not on real hardware that can fail in various ways or have unexpected race conditions or interacts with other places such as over the internet.

It has been quite well proven (think Kurt Gödel) that any system as complex as just arithmetic can have propositions that can neither be proven as true or as false and could be either. So there will be logical setups, written perhaps into the form of programs, that cannot be proven to work right, or even just halt someday when done.

The real question is way more detailed and complex. How does one create a complex program while taking care to minimize as well as you can the chances it is flawed under some conditions. There are walls of books written on such topics and they range from ways to write the software, perhaps in small modules that can be tested and then combined into larger subunits that can also be tested. There are compilers/interpreters/linters and sometimes ways of declaring your intentions to them, that can catch some kinds of possible errors, or force you to find another way to do things. You can hire teams of people to create test cases and try them or automate them. You can fill the code with all kinds of tests and conditionals even at run time that guarantee to handle any kinds of data/arguments handed to it and do something valid or fail with stated reasons. You can generate all kinds of logs to help establish the right things are happening or catch some errors.

But all that gets you typically is fewer bugs and software that is very expensive to create and decades to produce and by that time, you have lost your market to others who settle for less.

Consider an example of bit rot. I mean what if your CPU or hard disk has a location where you can write a byte and read it back multiple times and sometimes get the wrong result. To be really cautions, you might need your software to write something in multiple locations and when it reads it back in, check all of them and if most agree, ignore the one or two that don't while blocking that memory area off and moving your data elsewhere. Or consider a memory leak that happens rarely but if a program runs for years or decades, may end up causing an unanticipated error.

You can only do so much. So once you have some idea what language you want to use and what development environment and so on, research what tools and methods are available and see what you can afford to do. But if you have also not chosen your target architecture and are being asked to GUARANTEE things from afar, that opens a whole new set of issues.

I was on a project once where we had a sort of networked system of machines exchanging things like email and we tested it. A while later, we decided to buy and add more machines of a new kind and had a heterogeneous network. Unfortunately, some tests had not been done with messages of a size that turned out to not be allowed on one set of machines as too big but were allowed on the other that had a higher limit. We caught the error in the field when a message of that size was sent and then got caught in junkmail later as the receiving or intermediate machine was not expecting to be the one dealing with it. We then lowered the maximum allowed size on all architectures to the capacity of the weakest one.

This reminds me a bit of questions about languages that are free and come pretty much without guarantees or support. Is it safe to use them? I mean could they be harboring back doors or spying on you? Will you get a guarantee they won't switch to a version 3.0 that is incompatible with some features your software used? The short answer is there are no guarantees albeit maybe you can purchase some assurances and services from some third party who might be able to help you with the open-source software.

Unless your project accepts the realities, why start?

-----Original Message-----
From: Python-list <python-list-bounces+avi.e.gross=gmail.com@python.org> On Behalf Of o1bigtenor via Python-list
Sent: Tuesday, October 24, 2023 7:15 PM
To: Thomas Passin <list1@tompassin.net>
Cc: python-list@python.org
Subject: Re: Question(s)

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.

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