There is plenty of software being written to very high standards of quality (formally verified real-time control software for rockets/power plants/etc comes to mind), but most of that is not available for free on the internet (or for $5/month as a SAAS) because you get what you pay for.
Even TLA+ analysis and proof of correctness doesn't stop things like "new zookeeper clients are pushing a lot of new writes => disk space needed for logs increases => across all the nodes in the zookeeper cluster => the entire formally correct cluster keeps falling over now but it didn't last week"
I meant more in the sense of the proofs in TAOCP - these are programs that don't interact with anything outside of the program itself, no non-specified input, so a lot simpler, no dates, no actual machine memory, just a little synthetic world defined by the language itself. Even TeX is imagined to be unchanging after Knuth's passing, and is basically unchanged since the 70s.
For sure the world has moved on, but we have lost the ability to have confidence in the software and have had to develop tools and ways of thinking inspired by biology.
The combination (old Python, new shared library) could have vulnerabilities that neither (old python, old shared library) nor (new python, new shared library) has.
The general approach of most projects and vendors at the bottom of the stack to not accept full responsibility for their part is striking. The amount of lying, faking, leaky abstractions, adapting but not 100% etc. is so immense it is a wonder we get something done at the higher levels of the stack at all. I cannot comprehend, how it is possible, to hammer the RAM in such a way, that you can affect neighboring cells charge until the information interpreted based on the amount of charge in the cells is changed. This should never ever be possible. I haven't seen any such disclaimer this was possible on the package or in the data sheet of any RAM module. The same is with changing the kind of magnetic recording in the same hard drive model without notification (or change in model name that would be more honest). And then there are "subtle" problems, like coil whine on mainboards or PSUs for no reason - we know how to fix this. These high pitched sounds can give you headaches without you hearing much or anything. There is no indication about it on the package and almost no review tests this. And the whole Meltdown and Spectre type of bugs is just the cherry on top with major performance regressions because of it. So how are you supposed to write reliable software on top of all this if just a tight loop might actually change the state of hardware in such a way that is becomes a problem? I mean, this is just crazy.
I'll never understand why people think they can write some software and it'll stay pristine forever. Even if it was had no known bugs at some point in the past, the world is a harsh place and your program, its dependencies, its programming language or even its OS can be found to be subtly broken at any moment. Even if it is not outright buggy, the world will change around you until the interfaces you depend on are no longer there. (looking at you, software program at $WORK that only works with PS/2 keyboards but not USB keyboards)