Comment by moomin

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.