To be clear, nothing I said has much to do with types: preconditions and postconditions are a more general notion and types are one way to approximate them in s

To be clear, nothing I said has much to do with types: preconditions and postconditions are a more general notion and types are one way to approximate them in such a way that they can be automatically checked. However, because of the halting problem, there will always be correct programs that cannot be typed.