Re: else ladders practice

On 19/11/2024 06:37, Janis Papanagnou wrote:

On 10.11.2024 16:13, David Brown wrote:

[...]

>
My preferences are very much weighted towards correctness, not
efficiency.  That includes /knowing/ that things are correct, not just
passing some tests. [...]

 I agree with you. But given what you write I'm also sure you know
what's achievable in theory, what's an avid wish, and what's really
possible.

Sure.  I've done my fair share of "write-test-debug" cycling for writing code - that's almost inevitable when interacting with something else (hardware devices, other programs, users, etc.) that are poorly specified.  At the other end of the scale, you have things such as race conditions, where is no option but to make sure the code is written correctly.
The original context of this discussion was about small self-contained functions, where correctness is very much achievable in practice - /if/ you understand that it is something worth aiming at.

Yet there's also projects that don't seem to care, where
speedy delivery is the primary goal. Guaranteeing formal correctness
had never been an issue in the industry contexts I worked in, and I
was always glad when I had a good test environment, with a good test
coverage, and continuous refinement of tests. Informal documentation,
factual checks of the arguments, and actual tests was what kept the
quality of our project deliveries at a high level.
 

There are a great variety of projects, and the development style differs wildly.  Ultimately, you want a cost-benefit balance that makes sense for what you are doing, and true formal proof methods are only cost-effective in very niche circumstances.  In my work, I have rarely used any kind of formal methods - but I constantly have the principles in mind.  When I call a function, I can see that the parameters I use are valid - and /could/ be proven valid.  I know what the outputs of the function are, and how they fit in with the calling code - and I use that to know the validity of the next function called.  If I can't see such things, it's time to re-factor the code to improve clarity.
Of course testing is important, at many levels.  But the time to test your code is when you are confident that it is correct - testing is not an alternative to writing code that is as clearly correct as you are able to make it.