Genuine question: how did this error get through? It seems really simple/basic and I thought that expressing a proof in a formal language was supposed to prevent this?
Disclaimer: I'm kinda familiar with the ideas of automatically provable software systems but haven't done anything with them myself. If I'm missing an obvious fact(s) here please let me know :)
I get that the proof is big and complicated, but "We messed up a +/- sign" kinda sounds like announcing that the next version of the Linux kernel is done ("Version 7.0.0 is awesome!") followed by realizing that it doesn't compile ("Turns out someone used 1 equals where they should have used 2. Stay tuned for V 7.0.01!").
Disclaimer: I'm kinda familiar with the ideas of automatically provable software systems but haven't done anything with them myself. If I'm missing an obvious fact(s) here please let me know :)
I get that the proof is big and complicated, but "We messed up a +/- sign" kinda sounds like announcing that the next version of the Linux kernel is done ("Version 7.0.0 is awesome!") followed by realizing that it doesn't compile ("Turns out someone used 1 equals where they should have used 2. Stay tuned for V 7.0.01!").
I've got to be missing something here :)