+1 on guest mode. Handing the headset to someone else is a high-friction point with the calibration that needs to be done on every swap. Oftentimes I want to show someone the current experience without needing to setup a mirror and handing over the headset is the most intuitive way to do so.
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.
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.
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.
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.
Got any ideas of books that address this? I'm generally curious about some frequent problems that pop-up all the time that would be easier solved by some theoretical algorithm like an SAT solver.
