Path: ...!weretis.net!feeder9.news.weretis.net!news.quux.org!eternal-september.org!feeder2.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: David Brown <david.brown@hesbynett.no>
Newsgroups: comp.lang.c
Subject: Re: else ladders practice
Date: Tue, 19 Nov 2024 09:19:18 +0100
Organization: A noiseless patient Spider
Lines: 49
Message-ID: <vhhhm7$1oeqa$1@dont-email.me>
References: <3deb64c5b0ee344acd9fbaea1002baf7302c1e8f@i2pn2.org>
 <vg0t3j$2ruor$1@dont-email.me>
 <78eabb4054783e30968ae5ffafd6b4ff2e5a5f17@i2pn2.org>
 <vg2g37$37mh3$1@dont-email.me> <6724CFD2.4030607@grunge.pl>
 <vg2llt$38ons$1@dont-email.me>
 <2491a699388b5891a49ef960e1ad8bb689fdc2ed@i2pn2.org>
 <b681ee05856e165c26a5c29bf42a8d9d53843d6d@i2pn2.org>
 <vg2ttn$3a4lk$1@dont-email.me> <vg33gs$3b8n5$1@dont-email.me>
 <vg358c$3bk7t$1@dont-email.me> <vg37nr$3bo0c$1@dont-email.me>
 <vg3b98$3cc8q$1@dont-email.me> <vg5351$3pada$1@dont-email.me>
 <vg62vg$3uv02$1@dont-email.me> <vg8a84$euka$1@dont-email.me>
 <vg8koq$gpsg$1@dont-email.me> <vgat50$112jp$1@dont-email.me>
 <vgb8if$13ioj$1@dont-email.me> <vgbhkt$155v2$1@dont-email.me>
 <vgn0vl$3kr82$1@dont-email.me> <vgnfnd$3nmui$1@dont-email.me>
 <vgpcdv$7jqv$1@dont-email.me> <vgqiii$edif$1@dont-email.me>
 <vhh86t$1mtjb$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Tue, 19 Nov 2024 09:19:19 +0100 (CET)
Injection-Info: dont-email.me; posting-host="5a8782e9fffd78b6d7e1a9b3aea4b0ae";
	logging-data="1850186"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX182uhF5Lu/+zxe6696+AeJsy8fwOJ6R/fM="
User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:102.0) Gecko/20100101
 Thunderbird/102.11.0
Cancel-Lock: sha1:VKkHbj6PvKBEFUSBkVrHflY8j+8=
In-Reply-To: <vhh86t$1mtjb$1@dont-email.me>
Content-Language: en-GB
Bytes: 4386

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.