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

141–150 of 163 posts

Re: Programmers should never trust anyone, not even themselves

#141

Post by agentultra »

mbonnet wrote: post #135
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…

Formal verification is nice, but requires crazy skilled people at high cost. It's not always practical/feasible to have as part of your SWE process.

And it's not necessary for every project.

It's nice to have when it is though.

The cost is coming down. Proof automation is incredible today and rapidly improving. This is the part that does the tedious parts of a proof for you so that you can focus on the theorems that matter. The languages and proof systems themselves are easier than ever to pick up and use which is bringing the skill cost down.

I don't think most software projects need a huge, dedicated team of specialists to benefit from formal software verification.

Re: Programmers should never trust anyone, not even themselves

#144

Post by will1am »

blitzar wrote: post #45
eru wrote: post #28

Earlier quoted context omitted.

I guess you need to compartmentalise into different kinds of 'trust'. The not 'trusting' you do with a computer is different from the trusting you do with fellow humans in daily life. They just happen to use the same word in English.

I trust the computer far more than the fellow humans. The computer will generally give a predictable output for a given input. "fellow humans in daily life" .... not so much.

Human variability and unpredictability can also be a source of creativity. But I understand you completely

Re: Programmers should never trust anyone, not even themselves

#145

Post by will1am »

eru wrote: post #58
blitzar wrote: post #45

Earlier quoted context omitted.

I trust the computer far more than the fellow humans. The computer will generally give a predictable output for a given input. "fellow humans in daily life" .... not so much.

I hope you never have to cross a street, or get anywhere near a car with a human behind the wheel.

That's why I don't have a driver's license

Re: Programmers should never trust anyone, not even themselves

#146

Post by senkora »

agentultra wrote: post #136
atrus wrote: post #134

Earlier quoted context omitted.

> 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 that shouldn't mean we cannot make progress. But this seems like an argument against formal verification. Formal verification is 100x harder than writing tests...and still doesn't guarantee correctness? Those axiom wrenches are sti…

It guarantees correctness vis. the axioms chosen. That's a much more powerful statement and guarantee than a unit test which only exercises a single example. A formal proof that an algorithm makes progress, doesn't require a lock, or whatever property the proof is arguing is 100% guaranteed for every case. For example, a simple function over the set of integers. A unit test can only test individual elements of the se…

Agreed.

A good set of unit tests partitions the input space into parts, and then provides an existence proof that the program is correct for an example chosen from each part.

A good formal proof does the same, but provides a universal proof that the program is correct for all examples chosen from each part.

Both strategies can fail if they miss an important part of the input set. Unit tests can also fail if a program is “adversarial” and fails in a specific input that isn’t the particular example.

In practice, achieving “a good set of unit tests” requires you to mentally work out how to partition the input set in a way that matches your program, and at that point you’re most of the way to proving it correct, so you might as well do that. It still might make sense to write unit tests if you don’t have the tooling to enforce a mechanical proof.

Re: Programmers should never trust anyone, not even themselves

#147

Post by getpost »

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…

> Don't be paranoid.

How do you mean? I think the article (and my experience) suggests that you do have to be paranoid. [I looked up paranoid, just to be sure I knew the exact definition, and I didn't. It's an "extreme and irrational" fear. Is looking it up parnoid? Hahaha.] Colloquially, paranoia is extreme and not necessarily irrational. Think of Andy Grove, "Only the paranoid survive." Or Kurt Kobain, "Just because you are paranoid, it doesn't mean they're not after you."

Anyway, the way I frame the issue of software quality, is to hold the view that there are always errors, and the best you can do to apply extreme vigilance in attempting to ensure errors occur rarely.

Re: Programmers should never trust anyone, not even themselves

#148

Post by globular-toast »

IshKebab wrote: post #140
globular-toast wrote: post #38

Earlier quoted context omitted.

The deposits aren't assets to the bank, they are liabilities. The loans are their assets (your liability is their asset). They don't need to "do anything" with your deposit because it doesn't exist. If I increment the number 2 to the number 4, have I brought something into existence, in particular 2 "things"? What is that? Why can't I just bring 3 things into existence without incrementing the initial number? If this…

> They don't need to "do anything" with your deposit because it doesn't exist. Uhm yeah they do. If they take my money and then just do nothing with it then they won't make any money from it. Banks invest your money. (I don't think that's the main way they make money - it's probably mostly from credit card interest, but they definitely do it.) The money you pay into banks absolutely exists in every sense. Banks can c…

You're wrong, but you're far from alone. Essentially the way the whole finance industry works is there is an enormous gulf between their understanding of money and the general public's understanding. They don't contribute anywhere near as much to society as people think, in fact they fuck a lot of things up, but they run the books, of course they'll come out on top.

There's a great intro to how banking really works today here: https://positivemoney.org/how-money-works/banking-101-video-...

Re: Programmers should never trust anyone, not even themselves

#149

Post by mistermann »

leecommamichael wrote: post #14

What does it do to the psyche, to not be able to trust anyone?

Yet another very important portion of reality that science hasn't gotten around to yet. Perhaps we'll find the answer a bit further out in the universe, or deeper inside matter.

Re: Programmers should never trust anyone, not even themselves

#150

Post by lpribis »

bitwize wrote: post #106
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…

"Trust, but verify" comes from the Soviet Union and is an example of Russian humor. It helps that the Russian words for "trust" and "verify" rhyme. It really means something like "act like you trust the person, but secretly, don't trust them and double check that they've fulfilled their commitments". Putting on a smiling face and acting as if everybody was acting in good faith, while secretly expecting the stab in th…

"doveryay, no proveryay".

It rolls off the tounge so much better in Russian.

Post reply on HN