4 ms·

Everybody makes mistakes writing any kind of function.

by kleiba 5y ago

junon 5y ago
God I'm so tired of this take. "All code has bugs." "Everyone writes shitty code, some just make it less shitty." ad nauseum. I don't know where this started (more, when it got popular) but it's such a cop out and lazy argument to anything safety-related. It adds nothing to the discussion and provides no insight or substance, yet people parrot it often, especially around "language lawyer"-type HN articles. Moreover, it's wrong. Not every function has a bug. Yes, there are ways to prove this. No, not every function needs to protect against the computer being struck by lightning, or any other fault, in every case. It's such a weird and wrong argument and it's always said with such confidence.
- sethammons 5y ago
  The idea that all software is terrible or all code has bugs is leveraged at my work as a form of psychological safety. "Yes, 'all' software has bugs, so you should feel safe exposing a bug you made and we can all learn from it." A person who took the saying as an excuse to be sloppy would get called out hard on our teams and wouldn't last if they kept that view.
- Levitz 5y ago
  I think every code has bugs in the same way that every gun is always loaded. Yes you can throughly check for it in some place and be rather sure that it's not loaded, but the way to act around it is as if it could always be loaded. This doesn't excuse writing buggy code, same as you should always handle a gun with care, but it promotes good behaviour around it.
  - junon 5y ago
    This is nonsense. Comparing the two makes no sense. > Yes you can throughly check for it in some place and be rather sure Look up formal verification. You can prove, mathematically, that code is bug free.
    - vntok 5y ago
      No, that does not follow, it is actually a common logical flaw. What you can prove with formal verification is that the code conforms to the sacro-saint spec. But who says the spec is bug-free?
    - gnulinux 5y ago
      I write code in Agda (a proof assistant) for a living and this is rarely true. Because (1) even if you prove your program is correct as per spec it doesn't prove it's correct according to user/PM since spec can/will be buggy (2) proving every single theorem about your system is an extraordinary time sink, an engineer needs to know what parts are higher risk and needs to be proven and which parts are corrolaries of basic algebra and proving is of academic interest. EDIT: In my experience the biggest benefit you get from proof assistants like Coq, Agda etc is being able to run arbitrary unittests within your type system. It's convenient because it makes all bugs a type error and therefore possible to check at compile time. This doesn't mean agda will magically find all bugs, but it means you have more tools to do so.
      - junon 5y ago
        Bugs in spec != bugs in code. This is expressly moving the goalposts.
        gnulinux 5y ago
        Even if this were true my point (2) still stands. But it really isn't true because spec is part of the code. If your formalism is wrong, irregardless of whether implementation is correct, your code will behave wrong. There is absolutely no goal post moving. If my program is wrong, I can't tell my user "well, my unittests are all passing and I have 100% code coverage".
        junon 5y ago
        > Even if this were true my point (2) still stands. And it is completely beside the point of the original argument. I was never arguing against your second point.
- jusssi 5y ago
  You can formally prove that a function always does exactly what the author intended, no less, no more. But it still might be the wrong thing to do. The question is, do you count that as a bug or something else.
  - junon 5y ago
    That's moving the goalposts, and not the point originally being made nor the point I'm addressing.
- commandlinefan 5y ago
  > Not every function has a bug Ok, you're right. Every non-trivial function has a bug.

Everybody makes mistakes writing any kind of function.

by kleiba 5y ago

Everybody makes mistakes writing any kind of function.

God I'm so tired of this take. "All code has bugs." "Everyone writes shitty code, some just make it less shitty." ad nauseum. I don't know where this started (more, when it got popular) but it's such a cop out and lazy argument to anything safety-related. It adds nothing to the discussion and provides no insight or substance, yet people parrot it often, especially around "language lawyer"-type HN articles. Moreover, it's wrong. Not every function has a bug. Yes, there are ways to prove this. No, not every function needs to protect against the computer being struck by lightning, or any other fault, in every case. It's such a weird and wrong argument and it's always said with such confidence.

sethammons 5y ago
The idea that all software is terrible or all code has bugs is leveraged at my work as a form of psychological safety. "Yes, 'all' software has bugs, so you should feel safe exposing a bug you made and we can all learn from it." A person who took the saying as an excuse to be sloppy would get called out hard on our teams and wouldn't last if they kept that view.
Levitz 5y ago
I think every code has bugs in the same way that every gun is always loaded. Yes you can throughly check for it in some place and be rather sure that it's not loaded, but the way to act around it is as if it could always be loaded. This doesn't excuse writing buggy code, same as you should always handle a gun with care, but it promotes good behaviour around it.
- junon 5y ago
  This is nonsense. Comparing the two makes no sense. > Yes you can throughly check for it in some place and be rather sure Look up formal verification. You can prove, mathematically, that code is bug free.
  - vntok 5y ago
    No, that does not follow, it is actually a common logical flaw. What you can prove with formal verification is that the code conforms to the sacro-saint spec. But who says the spec is bug-free?
  - gnulinux 5y ago
    I write code in Agda (a proof assistant) for a living and this is rarely true. Because (1) even if you prove your program is correct as per spec it doesn't prove it's correct according to user/PM since spec can/will be buggy (2) proving every single theorem about your system is an extraordinary time sink, an engineer needs to know what parts are higher risk and needs to be proven and which parts are corrolaries of basic algebra and proving is of academic interest. EDIT: In my experience the biggest benefit you get from proof assistants like Coq, Agda etc is being able to run arbitrary unittests within your type system. It's convenient because it makes all bugs a type error and therefore possible to check at compile time. This doesn't mean agda will magically find all bugs, but it means you have more tools to do so.
    - junon 5y ago
      Bugs in spec != bugs in code. This is expressly moving the goalposts.
      - gnulinux 5y ago
        Even if this were true my point (2) still stands. But it really isn't true because spec is part of the code. If your formalism is wrong, irregardless of whether implementation is correct, your code will behave wrong. There is absolutely no goal post moving. If my program is wrong, I can't tell my user "well, my unittests are all passing and I have 100% code coverage".
        junon 5y ago
        > Even if this were true my point (2) still stands. And it is completely beside the point of the original argument. I was never arguing against your second point.
jusssi 5y ago
You can formally prove that a function always does exactly what the author intended, no less, no more. But it still might be the wrong thing to do. The question is, do you count that as a bug or something else.
- junon 5y ago
  That's moving the goalposts, and not the point originally being made nor the point I'm addressing.
commandlinefan 5y ago
> Not every function has a bug Ok, you're right. Every non-trivial function has a bug.