Nope, my problem isn&#x27;t reasoning about the lower level components. In fact you can assume I have correctness proofs for every piece of the infrastructure. What I don&#x27;t have is the higher-level piece that can reason about the lower level components and do so when new pieces are added, old pieces removed, new guarantees enforced, old ones relaxed, etc. A static type system no matter how advanced doesn&#x27;t help with any of it.