Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Programmers should never trust anyone, not even themselves

carbon-steel.github.io

Post reply on HN
Print view View original

121–130 of 163 posts

Re: Programmers should never trust anyone, not even themselves

#121

Post by agentultra »

n4r9 wrote: post #119
agentultra wrote: post #113

Earlier quoted context omitted.

This is addressed by the de Bruijn Criterion. The essential idea is that a small number of "trusted" rules should be enough to satisfy even the largest proofs. You have to keep the number of rules small enough that they can be reviewed and understood by humans so that you can trust the proofs verified by the kernel.

That probably helps to reduce the occurrence of issues, but I feel you are still ultimately relying on the correctness of proof assistants like Coq. And I am sure that bugs are occasionally found in Coq!

Indeed it does happen and it's unavoidable. You have to pick your axioms from somewhere and sometimes we pick the wrong ones or we find errors in our definitions. There's no "complete" or "perfect" system.

Re: Programmers should never trust anyone, not even themselves

#122

Post by simonw »

This is why I try to have my code commits bundle tests along with any corresponding implementation changes. The job of the test is to PROVE that the updated implementation code did what it was supposed to do - both now and into the future.

If the test doesn't do that - if it still passes even if you revert the implementation - then the test isn't doing its job.

Re: Programmers should never trust anyone, not even themselves

#123

Post by mistermann »

> So if abstractions can be problematic, then should we try to understand a topic without abstractions (to know cars as they really are)? No. When you dig beneath abstractions, you just find more abstractions.

Demonstrating that language and colloquial "logic" are also abstractions.

> It’s turtles all the way down.

Memes and catch phrases are abstractions.

> These layers of abstractions go down until we hit our most basic axioms about logic and reality.

Reality too is an abstraction. Luckily all humans run Faith, and it runs invisibly, otherwise I suspect we'd have not made it this far. Though, it now seems like that which saved us may now take us down (climate change, nuclear weapons, other/unknown).

> Trust, but verify.

Haha...of course, just use logic and critical thinking!

Re: Programmers should never trust anyone, not even themselves

#124

Post by mistermann »

kryptiskt wrote: post #48

I think "trust, but verify" (as mentioned in the article) is a much more useful motto than "never trust anyone". The latter isn't an useful attitude, if you took it seriously you would have carefully check or rewrite everything from the ground up. And then you'd either have to trust the hardware anyway or enlist in a course on VLSI design. "Trust, but verify" is much more practicable, at least if you don't feel the n…

> I think "trust, but verify" (as mentioned in the article) is a much more useful motto than "never trust anyone". The latter isn't an useful attitude, if you took it seriously you would have carefully check or rewrite everything from the ground up.

Not actually. You're describing an abstraction: your opinion/perception of what must/can be done.

It is possible to be comfortable with uncertainty and the unknown (everyone already is, but only in certain, intuitive (in large part due to cultural conditioning, which comes in a variety of forms) ways), it's mainly just counter-culture and counter-intuitive, thus needs strategies, and practice(!) (plus some non-trivial multi-level, multi-dimensional recursion....this is what us HN folks are good at, and love though, right? Right?[1]). We've all been through the hard work at least once, in a certain (mostly) shared way. There are other ways though.

> "Trust, but verify" is much more practical

How do you verify your verification in complex scenarios though? I bet I know: trust/contentment (in your verification skills), though this layer typically is not revealed to us, so causes no psychological unrest ("all is well"), because it does not exist.

> Don't be paranoid.

What do you think your reaction would be if you discovered this is not just wrong, but backwards?

[1] Alternatively: maybe we are only good at it, and only love it, sometimes? But then, "we" is a complex and deep set, into which we have little insight, but also plenty of hallucinated "insight".

Re: Programmers should never trust anyone, not even themselves

#125

Post by mistermann »

tm11zz wrote: post #25

This is a really useful mindset as a programmer, but backfires in real-life as it makes you an anxious person.

> but backfires in real-life as it makes you an anxious person.

If I was to point out this is an approximation, or a tautology (it is only true to the degree that it is true, which is not (necessarily[1]) 100% of the time), would it make you anxious? And if so, do you think it wouldn't be possible for you to learn [1] a new approach so it does not make you anxious?

Re: Programmers should never trust anyone, not even themselves

#126

Post by bobthepanda »

thfuran wrote: post #68
dartos wrote: post #65

Earlier quoted context omitted.

> Unpopular opinion, but I always say that unit tests are contracts for the API You’re talking about integration tests or e2e tests. Those don’t sound like unit tests.

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.

Re: Programmers should never trust anyone, not even themselves

#127

Post by atoav »

As an electronics guy this is really ingrained. Not only could you easily waste days on a problem if you assume things rather than check them, in some cases you might also get a painful experience or depending on what you're working on that mistake might even be your last, burn down a house, kill others or what not. Checking your priors is one thing, ensuring your stuff fails gracefully if they are abnormal another. Meanwhile most software won't even handle a network disconnect gracefully.

As more and more stuff™ is moving from hardware into software, for totally understandable reasons, the absolute number of software that could absolutely ruin human lifes is growing. This calls for higher standards when it comes to the whole field of software engineering.

Re: Programmers should never trust anyone, not even themselves

#128

Post by skydhash »

pcwelder wrote: post #6

High quality article with some new advices. > Read more documentation than just the bare minimum you need I wish I practiced this before, I'd be as good and quick as some of my brilliant colleagues.

I love it when projects gave single HTML documentation or a PDF. In the worst case, I'd take a nice site like Laravel's documentation. Any piece of software I use, I try to do a speed reading of the whole documentation or a significant part if it's big. A mental model of all the offered features is a nice help when solving problems.

Re: Programmers should never trust anyone, not even themselves

#129

Post by skydhash »

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).

It's not impossible to verify it, it's impossible to automatically verify it with another program. Other issues are the underlying abstract machine (which can have its own bugs) and the surrounding environment (you either need to assert or/and sanitize your inputs).

Re: Programmers should never trust anyone, not even themselves

#130

Post by bee_rider »

agentultra wrote: post #115

To me, this is the argument for formal verification. I don't want to hear a hand-waving explanation that this algorithm will always complete. If the algorithm is sufficiently complex I want proof. Otherwise, why would I believe you? Abstractions, in the mathematical sense, always hold (unless there is a flaw in the definition itself). Axioms in any sense are always going to throw a wrench in things. Thank Godel. But…

I dunno. Even in some fairly math-y situations, line solving sparse linear systems, we get stuff like BiCGStab which often will work well and converge in cases where we can’t prove that it must.

CS seems mostly good for proving that everything is hopeless in the rigorous general case and, hey, here are some heuristics to give you hope again.

Post reply on HN