zlacker

> The people at Twitter who understood the system and could predict the side effects were all fired or left

And never created sufficient testing.

>>humean+(OP)
Yes, because Elon Musk would never scrap existing pre-release testing procedures.

>>humean+(OP)
There is never sufficient testing. If there is, then you have a formal proof for your algorithm.

>>humean+(OP)
You can't write tests for the changes someone might make in the future.

>>greent+B8
That's exactly why you write tests. You want to be sure future changes don't break present functionality, especially if the future changes are being done by someone who doesn't understand your part of the system.

>>whatev+13
Beware of bugs in the above code; I have only proved it correct, not tried it. – Donald Knuth

It's not just hypothetical either. There was a bug in a sorting algorithm a few years back that had been 'proved' correct. I think it was to do with numbers wrapping, and that hadn't been considered in the mathematical proof.

>>onion2+8m
But if you need to make an update to a core system that'll necessitate updating the tests and you're back to flying blind.

>>Sketch+fe1
It shouldn't require updating the tests, so long as you're testing the functionality rather than the implementation.

>>kybern+dU
WPA2 also had an exploit (KRACK) while the handshake algorithm itself was "proven to be secure". Formal verification is a powerful tool but it does not guarantee bug-free code: it merely guarantees that the particular bugs you checked for are not possible.

>>onion2+8m
You write tests for your code as it exists to make sure it functions. You cannot write tests for every conceivable change that someone else might make in the future that either mis-uses your code or adds new code inbetween that didn't previously exist. You need the people who add that new code to write new tests. Something that it seems the remaining engineers at Twitter do not have time for.