3 ms·

Formal methods are to programming like ropes are to mountain climbing. >Whether you use functional programming or dynamic typing it only affects small, local p

by ummonk 8y ago

Formal methods are to programming like ropes are to mountain climbing. >Whether you use functional programming or dynamic typing it only affects small, local problems in the practice of climbing mountains. Static typing is a type of formal method.

tsimionescu 8y ago
Yes, but the range of what 'static typing' means is so large that it is meaningless in this case. C is statically typed, and so are Java and OCaml. So is Idris. Of these, only Idris' type system has any power to model truly interesting properties (though the cost of doing so, in program complexity, is huge). Otherwise, even something as simple as rejecting `add(x, y) return x - y;` as a well typed function is beyond all of the others.
- ummonk 8y ago
  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”?
  - deleted 8y ago
    [deleted]
  - tsimionescu 8y ago
    No, I'm saying that there is no way to encode even such a simple property as 'addition of two numbers produces a bigger number' in the type systems of most languages out there (including stuff like the ML family), which is probably why (non-dpendent/linear/other advanced) type systems have never been shown to improve program correctness the way other formal techniques have. Even simple type systems help in other ways (ease of development, documentation, performance).

by ummonk 8y ago

tsimionescu 8y ago

Yes, but the range of what 'static typing' means is so large that it is meaningless in this case. C is statically typed, and so are Java and OCaml. So is Idris. Of these, only Idris' type system has any power to model truly interesting properties (though the cost of doing so, in program complexity, is huge). Otherwise, even something as simple as rejecting `add(x, y) return x - y;` as a well typed function is beyond all of the others.

ummonk 8y ago
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”?
- deleted 8y ago
  [deleted]
- tsimionescu 8y ago
  No, I'm saying that there is no way to encode even such a simple property as 'addition of two numbers produces a bigger number' in the type systems of most languages out there (including stuff like the ML family), which is probably why (non-dpendent/linear/other advanced) type systems have never been shown to improve program correctness the way other formal techniques have. Even simple type systems help in other ways (ease of development, documentation, performance).