5 ms·

The writing is really enjoyable. > Programming in this state is like living life surrounded by a force field that protects you from all harm. [...] We deleted

by Rygian 3y ago

The writing is really enjoyable. > Programming in this state is like living life surrounded by a force field that protects you from all harm. [...] We deleted all of our dependencies (including Zookeeper) because they had bugs, and wrote our own Paxos implementation in very little time and it _had no bugs_. Being able to make that statement and back it by evidence must be indeed a cool thing.

llm_trw 3y ago
I have proved my code has no bugs according to the spec. I do not make the claim my spec has no bugs.
- deleted 3y ago
  [deleted]
- yasuocidal 3y ago
  "Its not a bug, its a feature"
- coldtea 3y ago
  With formal proof systems, you can also claim that for your spec.
  - svieira 3y ago
    A formal proof is only as good as what-you-are-proving maps to what-you-intended-to-prove.
  - AlotOfReading 3y ago
    I've written formal proofs with bugs more than once. Reality is much messier than you can encode into any proof and there will ultimately be a boundary where the real systems you're trying to build can still have bugs. Formal verification is incredibly, amazingly good if you achieve it, but it's not the same as "perfect".
  - llm_trw 3y ago
    No you can't. You can claim that your spec doesn't violate some invariants in a finite number of steps, you can't claim that the spec contains all the invariants the real system must have and that it doesn't violate them in number of steps + 1.
  - cortesoft 3y ago
    This doesn't track with the real world, though. If you are writing software, it is almost always trying to accomplish a goal outside of itself. It is trying to solve a problem for someone, and how that problem can or should be solved is rarely perfectly clear. The spec is supposed to map to a real world problem, and there is never going to be a way to formalize that mapping.
btrettel 3y ago
The earliest that I've seen the attitude that one should eliminate dependencies because they have more bugs than internally written code was this book from 1995: https://store.doverpublications.com/products/9780486152936 https://store.doverpublications.com/products/9780486152936 pp. 65-66: > The longer I have computed, the less I seem to use Numerical Software Packages. In an ideal world this would be crazy; maybe it is even a little bit crazy today. But I've been bitten too often by bugs in those Packages. For me, it is simply too frustrating to be sidetracked while solving my own problem by the need to debug somebody else's software. So, except for linear algebra packages, I usually roll my own. It's inefficient, I suppose, but my nerves are calmer. > The most troubling aspect of using Numerical Software Packages, however, is not their occasional goofs, but rather the way the packages inevitably hide deficiencies in a problem's formulation. We can dump a set of equations into a solver and it will usually give back a solution without complaint - even if the equations are quite poorly conditioned or have an unsuspected singularity that is distorting the answers from physical reality. Or it may give us an alternative solution that we failed to anticipate. The package helps us ignore these possibilities - or even to detect their occurrence if the execution is buried inside a larger program. Given our capacity for error-blindness, software that actually hides our errors from us is a questionable form of progress. > And if we do detect suspicious behavior, we really can't dig into the package to find our troubles. We will simply have to reprogram the problem ourselves. We would have been better off doing so from the beginning - with a good chance that the immersion into the problem's reality would have dispelled the logical confusions before ever getting to the machine. I suppose whether to do this depends on how rigorous one is, how rigorous certain dependencies are, and how much time one has. I'm not going to be writing my own database (too complicated, multiple well-tested options available) but if I only use a subset of the functionality of a smaller package that isn't tested well, rolling my own could make sense.
- voidmain 3y ago
  In the specific case in question, the biggest problem was that dependencies like Zookeeper weren't compatible with our testing approach, so we couldn't do true end to end tests unless we replaced them. One of the nice things about Antithesis is that because our approach to deterministic simulation is at the whole system level, we can do it against real dependencies if you can install them. I was a co-founder of both FoundationDB and Antithesis.
deleted 3y ago
[deleted]

by Rygian 3y ago

llm_trw 3y ago

I have proved my code has no bugs according to the spec. I do not make the claim my spec has no bugs.

deleted 3y ago
[deleted]
yasuocidal 3y ago
"Its not a bug, its a feature"
coldtea 3y ago
With formal proof systems, you can also claim that for your spec.
- svieira 3y ago
  A formal proof is only as good as what-you-are-proving maps to what-you-intended-to-prove.
- AlotOfReading 3y ago
  I've written formal proofs with bugs more than once. Reality is much messier than you can encode into any proof and there will ultimately be a boundary where the real systems you're trying to build can still have bugs. Formal verification is incredibly, amazingly good if you achieve it, but it's not the same as "perfect".
- llm_trw 3y ago
  No you can't. You can claim that your spec doesn't violate some invariants in a finite number of steps, you can't claim that the spec contains all the invariants the real system must have and that it doesn't violate them in number of steps + 1.
- cortesoft 3y ago
  This doesn't track with the real world, though. If you are writing software, it is almost always trying to accomplish a goal outside of itself. It is trying to solve a problem for someone, and how that problem can or should be solved is rarely perfectly clear. The spec is supposed to map to a real world problem, and there is never going to be a way to formalize that mapping.

btrettel 3y ago

The earliest that I've seen the attitude that one should eliminate dependencies because they have more bugs than internally written code was this book from 1995: https://store.doverpublications.com/products/9780486152936 https://store.doverpublications.com/products/9780486152936 pp. 65-66: > The longer I have computed, the less I seem to use Numerical Software Packages. In an ideal world this would be crazy; maybe it is even a little bit crazy today. But I've been bitten too often by bugs in those Packages. For me, it is simply too frustrating to be sidetracked while solving my own problem by the need to debug somebody else's software. So, except for linear algebra packages, I usually roll my own. It's inefficient, I suppose, but my nerves are calmer. > The most troubling aspect of using Numerical Software Packages, however, is not their occasional goofs, but rather the way the packages inevitably hide deficiencies in a problem's formulation. We can dump a set of equations into a solver and it will usually give back a solution without complaint - even if the equations are quite poorly conditioned or have an unsuspected singularity that is distorting the answers from physical reality. Or it may give us an alternative solution that we failed to anticipate. The package helps us ignore these possibilities - or even to detect their occurrence if the execution is buried inside a larger program. Given our capacity for error-blindness, software that actually hides our errors from us is a questionable form of progress. > And if we do detect suspicious behavior, we really can't dig into the package to find our troubles. We will simply have to reprogram the problem ourselves. We would have been better off doing so from the beginning - with a good chance that the immersion into the problem's reality would have dispelled the logical confusions before ever getting to the machine. I suppose whether to do this depends on how rigorous one is, how rigorous certain dependencies are, and how much time one has. I'm not going to be writing my own database (too complicated, multiple well-tested options available) but if I only use a subset of the functionality of a smaller package that isn't tested well, rolling my own could make sense.

voidmain 3y ago
In the specific case in question, the biggest problem was that dependencies like Zookeeper weren't compatible with our testing approach, so we couldn't do true end to end tests unless we replaced them. One of the nice things about Antithesis is that because our approach to deterministic simulation is at the whole system level, we can do it against real dependencies if you can install them. I was a co-founder of both FoundationDB and Antithesis.

deleted 3y ago

[deleted]