3 ms·
Just to add to this, the better terms to use are "static" and "dynamic". Going with the example of a sound type system, a language could have a sound type syst
by ben-schaaf 9y ago
Just to add to this, the better terms to use are "static" and "dynamic".
Going with the example of a sound type system, a language could have a sound type system that does the actual checking at runtime.
- dozzie 9y agoNo, not really. Even though there's no good definition what "strong" and "weak" means, it was always meant as a totally different axis than static/dynamic typing. C is weakly typed, OCaml is strongly typed. Both are typed statically.
- catnaroek 9y agoA type soundness theorem is always of the form “a well-typed program never does such and such”. It relates the static semantics (type checking) to the dynamic semantics (operational semantics) of a programming language. It doesn't make any sense to talk about soundness for dynamic languages, because there's no static semantics to relate to the dynamic semantics.