Programmers should never trust anyone, not even themselves • Hacker News Board

Re: Programmers should never trust anyone, not even themselves

#161

Post by throwaway2037 » Fri, Jul 05, 2024, 7:50 AM UTC

drewcoo wrote: post #138

atribecalledqst wrote: post #60

> Failing tests indicate the presence of bugs, but passing tests do not promise their absence. As somebody who primarily lives on the testing side of the house, I've definitely run into cases where the developer promises that their unit tests will make a new feature less buggy, then about 5 minutes later I either find a mistake in the test or I find a bug in something that the developer didn't think to test at all. I…

Tests don't find bugs. They find things a developer needs to investigate. Most tests I've seen aren't aids to diagnosability, so if there is a bug, the developer is still needed to find it. > tests are written too early, using a data structure that gets changed in development I wouldn't call this "too early," but "testing the wrong thing" if they were testing internal particulars instead of behaviors.

    > Tests don't find bugs.

I want to be make sure I understand your message here. When I write unit tests, I frequently find bugs in my own code. Are you talking about something different?

Re: Programmers should never trust anyone, not even themselves

#162

Post by thfuran » Sun, Jul 07, 2024, 4:19 PM UTC

bobthepanda wrote: post #126

thfuran wrote: post #68

Earlier quoted context omitted.

Your units don't have some interface through which they interact with other units?

API is accesible public interface, I feel like I’ve seen it used to talk about accessible “to the public/other teams” from a service standpoint but not to describe any sundry public methods of a file.

No, it's application programming interface.

Re: Programmers should never trust anyone, not even themselves

#163

Post by versteegen » Sun, Jul 14, 2024, 4:45 AM UTC

tpm wrote: post #19

psychoslave wrote: post #16

> verifying code correctness is impossible Somehow, taking into account the state of our industry, yes. But this is not an absolute truth. I mean, we do have the theoretical frameworks and even tools to come with solutions that allow to proof that code is correct. It’s just that mapping this "know how" with the "how to deal with the expected flow rate feature" is very uncommon.

It is an absolute truth in the sense that it is true for all code that was not specifically written to be formally proven correct. So, given an arbitrary piece of code, it's impossible to verify it (because of the halting problem).

Those assertions are a long way off absolutely true!

The undecidability of Turing machines in general doesn't say you can't reason about any programs, as you seem to claim, it says there exists programs which have unverifiable behaviour.

(Although the proof provides unnatural examples, in practice simple recursive mathematical functions such as the Collatz conjecture will probably always be beyond automated analysis.)

Of course software that was not written with verification in mind can be verified correct, provided it doesn't contains things such as an interpreter or complex conditional recursion. There are static analysis tools for analysing programs in languages such as C++ which make use of ATPs (automated theorem provers). For example, most of zlib has been proven correct using Coq. Yes, verification of the entirety of complex programs is in general impossible, but parts of them can still be verified. It's the most common use of ATPs, and an active area of research!