> Note that functions like sin and cos have exactly the same type signature, yet it is disastrous if you mix them up. Static type checking doesn't help. I agre

> Note that functions like sin and cos have exactly the same type signature, yet it is disastrous if you mix them up. Static type checking doesn't help. I agree with you. I am hard-pressed to imagine types (where it's static analysis or anything at all) offering any help in catching inadvertent swaps of sin and cos. One thing that types could help with is avoiding confusion between e.g. radians and degrees. Even this I believe is quite a challenge, because the quintessential (in my opinion) example of static analysis and types as they arise in science and engineering, the SI units and dimensional analysis, take radians to be dimensionless and therefore do not distinguish the input and the output types of e.g. sin (Radians). I personally believe this problem is rectifiable beyond the SI type system (or who knows, within it), but not at no cost. I believe the choice to not distinguish the input and output types of e.g. sin (Radians) is rooted in many different practical considerations, and points to the difficulty of formalizing types in practice. > Test cases are therefore static checks. I don't agree with this unless you are talking about tests that perform some kind of symbolic execution / static analysis within them. What static analysis grants you is checking a "for all x" claim, without literally checking each x. You can argue that for any given static analysis system, the kinds of claims it lets you check are not that useful in practice, and I would agree in many situations. But having a finite number of test cases that tests some x is not the same as testing for all x.