Hacker News new | past | comments | ask | show | jobs | submit
I mean, he wasn’t using, or even envisaging, a language that could natively support proofs.

Personally I think proving Kubernetes, for instance, would be an exercise in pure frustration. There’s just too much to do.

Knuth seemed more interested in Tony’s notion of “obviously no bugs”. There always seemed to me to be a self-evident flavor to his literate code notions.

I say that as someone who sees Knuth as problematic in other respects starting in the 2010’s. Physics governs so much of computational complexity now that I think the idealized form he presents has transitioned from merely holding us back to being crippling. Only game designers, hyperscalers, and an esoteric few of the rest of us seem to understand the vast gulf between theory and practice that has developed in the five orders of magnitude that compute power has experienced since his first edition.

Many, many things that are considered constant in his world are instead logarithmic to the size of the data being managed, or in the case of very large data sets, order n^1/2 because of speed of light and thermodynamics. That vastly reorders the toolbox, because second shelf algorithms now rival or beat the top shelf ones and some options even farther down now become interesting for novel situations.

huh. Interesting background. Thanks for sharing.

Regarding your remark "[...] because second shelf algorithms now rival or beat the top shelf ones [...]". That is honestly something I would never have believed back in the 2000s, Windows XP era:

I thought we needed more than the classic mathematical operations and if/else for an operating system that drives the modern world like it had been envisioned by sci-fi in the past 100 years.

That turned out to be wrong: Your modern android with a couple of simple apps is everything a man from 1900 might ever conceivably want from technology.

And it is all if/else/while and mathematical operations.

It turned out you just needed enough of these, to get everything working nicely.

Watching in awe. Watching in awe.

Maybe that says something about kubernetes. Software systems that are complex enough to be intractable should probably be regarded as too complex to operate safely.
No, most software is this way.

https://www.galois.com/articles/specifications-dont-exist

I don't fully understand what you're objecting to. Are you saying it's not possible to build a formally verified container orchestration thing?

I do think that most software out there is unsafe. That doesn't make it useless, but if the effort required to exploit vulnerabilities is decreasing we will probably need to stop building things that way.