Formal systems obviously differ in their verification power and ease of use. E.g. with type systems, in terms of power on one end you have unsound type systems

Formal systems obviously differ in their verification power and ease of use. E.g. with type systems, in terms of power on one end you have unsound type systems and on the other end you have dependent types. Sound type systems with algebraic data types tend to be quite common though and reasonably powerful. As far as ease of use goes, type inference and flow analysis goes a very long way. >Otherwise, even something as simple as rejecting `add(x, y) return x - y;` as a well typed function is beyond all of the others. Why shouldn’t that be well typed (unless it is invoked with unsuitable argument types)? Are you saying the language should magically understand the english language meaning of “add”?