What is Expressiveness in a Computer Language

[rossberg at ps.uni-sb.de]

Joachim Durchholz write:
>
> Another observation: type safeness is more of a spectrum than a clearcut
> distinction. Even ML and Pascal have ways to circumvent the type system,

No. I'm not sure about Pascal, but (Standard) ML surely has none. Same
with Haskell as defined by its spec. OCaml has a couple of clearly
marked unsafe library functions, but no unsafe feature in the language
semantics itself.

> and even C is typesafe unless you use unsafe constructs.

Tautology. Every language is "safe unless you use unsafe constructs".
(Unfortunately, you can hardly write interesting programs in any safe
subset of C.)

> IOW from a type-theoretic point of view, there is no real difference
> between their typesafe and not typesafe languages in the "statically
> typed" column; the difference is in the amount of unsafe construct usage
> in practial programs.

Huh? There is a huge, fundamental difference: namely whether a type
system is sound or not. A soundness proof is obligatory for any serious
type theory, and failure to establish it simply is a bug in the theory.

- Andreas