I'm sure it is a fine program, don't get me wrong. But citing a Basic I program as something that is eternally true is exactly what I mean when talking about the world moving on. Does it even run on 64-bit operating systems? Will it keep working correctly after the unix timestamp goes beyond its signed 32 bit maximum and overflows? I'll also eat my hat if there is anything you can prove about it in the modern meaning of formal verification.
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.
NASA software is very good, but not in general formally verified, I think (based mostly on reading postmortems on various NASA failures).
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.
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.