Sure, you can use formal methods to prove properties that are hard to test. The point you seem to have missed is that it takes a lot of effort to do that.
The reality is that in most cases there's a cost benefit analysis regarding how much time you can spend on a particular feature and the strength of the guarantees.
>The Curry-Howard correspondence tells us to think of types as logical propositions with terms as their proofs.
Hence my point that you end up writing a metaprogram that emits the logic. Ensuring that the metaprogram is correct is a manual process. The more complex the proof, the harder it becomes to understand.
Consider Fermat's conjecture. It's trivial to state it, it's trivial to test it to be correct for a given set of inputs. However, proving it for the general case is quite difficult, and only a handful of people in the world can follow that proof.
> onsider Fermat's conjecture. It's trivial to state it, it's trivial to test it to be correct for a given set of inputs. However, proving it for the general case is quite difficult, and only a handful of people in the world can follow that proof.
This is a strawman, conventional static type system can't prove all general cases either and no body is saying that they do that. Yet, they being a superset of dynamic typing, they allow to have the same expesiveness as such by providing a bypass like 'Object' or 'any'.
The reality is that in most cases there's a cost benefit analysis regarding how much time you can spend on a particular feature and the strength of the guarantees.
>The Curry-Howard correspondence tells us to think of types as logical propositions with terms as their proofs.
Hence my point that you end up writing a metaprogram that emits the logic. Ensuring that the metaprogram is correct is a manual process. The more complex the proof, the harder it becomes to understand.
Consider Fermat's conjecture. It's trivial to state it, it's trivial to test it to be correct for a given set of inputs. However, proving it for the general case is quite difficult, and only a handful of people in the world can follow that proof.