Curry Howard just says that computation and proof simplification work similarly. Correctness has more to do with how rich your type system is and with how you take advantage of it during modeling (to rule out undesired program states as ill-typed)