Comparing Kubernetes to type systems is like comparing a shack to a gothic cathedral. Type systems are incredibly stable. They have to be proved both sound and complete via meticulous argumentation. Once proven such, they work and their guarantees exist... no matter what. If you avoid the use of the `unsafe...` functions in languages like Haskell, you can be guaranteed of all the things the type system guarantees for you. In more structured languages like Idris or Coq, there is an absolute guarantee even on termination. This does not break.
Whereas on kubernetes... things break all the time. There is no well-defined semantic model for how the thing works. This is a far cry from something like the calculus of inductive constructions (basis of COQ) for which there is a well-understood 'spec'. Anyone can implement COIC in their language if they understand the spec. You cannot say the same for kubernetes.
Kubernetes is a nice bit of engineering. But it does not provide the same guarantees as type systems. In fact, of the four 'complicated' things you mentioned, only one thing has a well-defined semantic model and mathematically provable guarantees behind it. GraphQL is a particular language (and not one based on any great algebra either, like SQL), Kubernetes is just a program, and unit tests are just a technique. None of them are abstract entities with proven, unbreakable guarantees.
Really, comparing Kubernetes to something like system FC or COIC is like comparing Microsoft Word to Stoke's theorem.
The last thing I'll say is that type systems are incredibly easy. There are a few rules to memorize, but they are applied systematically. The same is not true of Kubernetes. Kubernetes breaks constantly. Its abstractions are incredibly leaky. It provides no guarantees other than an 'eventually'. And it is very complicated. There are myriad entities. Myriad operations. Myriad specs, working groups, etc. Type systems are relatively easy. There is a standard format for rules, and some proofs you don't really need to read through if you trust the experts.
Whereas on kubernetes... things break all the time. There is no well-defined semantic model for how the thing works. This is a far cry from something like the calculus of inductive constructions (basis of COQ) for which there is a well-understood 'spec'. Anyone can implement COIC in their language if they understand the spec. You cannot say the same for kubernetes.
Kubernetes is a nice bit of engineering. But it does not provide the same guarantees as type systems. In fact, of the four 'complicated' things you mentioned, only one thing has a well-defined semantic model and mathematically provable guarantees behind it. GraphQL is a particular language (and not one based on any great algebra either, like SQL), Kubernetes is just a program, and unit tests are just a technique. None of them are abstract entities with proven, unbreakable guarantees.
Really, comparing Kubernetes to something like system FC or COIC is like comparing Microsoft Word to Stoke's theorem.
The last thing I'll say is that type systems are incredibly easy. There are a few rules to memorize, but they are applied systematically. The same is not true of Kubernetes. Kubernetes breaks constantly. Its abstractions are incredibly leaky. It provides no guarantees other than an 'eventually'. And it is very complicated. There are myriad entities. Myriad operations. Myriad specs, working groups, etc. Type systems are relatively easy. There is a standard format for rules, and some proofs you don't really need to read through if you trust the experts.