14 ms·

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 l

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

by Levitz 5y ago

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.