Do you mean logical? Types absolutely do prove logical correctness. In fact that’s all they do. However they can only prove the correctness of logic that’s typ

Do you mean logical? Types absolutely do prove logical correctness. In fact that’s all they do. However they can only prove the correctness of logic that’s type encoded. If your program is a primitive soup, there’s not much logic for them to prove.