4 ms·

> (all of which are functional, in part also because OO/subtyping is hard to reason about formally) OO/subtyping is NOT orthogonal to functional, nor is it inh

> (all of which are functional, in part also because OO/subtyping is hard to reason about formally) OO/subtyping is NOT orthogonal to functional, nor is it inherently at odds with formal reasoning. OCaml has both imperative and functional objects; Haskell, Mercury, and Coq (a formal logic language) all support typeclasses, which subsume most of OO and provide subtyping. Additionally, strong typing has little to do with formal reasoning as well (see: Lisp/Scheme/the lambda calculus). What makes functional languages amenable to formal methods is that they are functional and therefore referentially transparent. Mathematical proofs carry no implicit concept of "state"; hence if you are trying to prove anything about code in, say, C, you need to augment the code with explicit state and remove all non-local effects. (See: the Why language, which attempts to bridge this gap.) Algebraic/generalized-algebraic type constructors used by most functional languages don't hurt either, as they allow programs to construct complex terms without relying on lower-level stateful abstractions such as memory allocation.

Locke1689 13y ago
hence if you are trying to prove anything about code in, say, C, you need to augment the code with explicit state and remove all non-local effects. (See: the Why language, which attempts to bridge this gap.) Actually, you just need to augment your model with notions of state, which is standard in operational semantics. It can just be harder to prove things in a complex model, so theorists prefer simplification when possible.
tomp 13y ago
Not inherently, no, but practically, yes. The type system of, say, Java, isn't even formally sound; overridden functions can be covariant in parameter types, which would not be permissible in a proper subtype-based type system such as OCaml's.
- colanderman 13y ago
  Ah yes, I forgot about Java's failings in this area.

Locke1689 13y ago

hence if you are trying to prove anything about code in, say, C, you need to augment the code with explicit state and remove all non-local effects. (See: the Why language, which attempts to bridge this gap.) Actually, you just need to augment your model with notions of state, which is standard in operational semantics. It can just be harder to prove things in a complex model, so theorists prefer simplification when possible.

tomp 13y ago

Not inherently, no, but practically, yes. The type system of, say, Java, isn't even formally sound; overridden functions can be covariant in parameter types, which would not be permissible in a proper subtype-based type system such as OCaml's.

colanderman 13y ago
Ah yes, I forgot about Java's failings in this area.