Are there any programming languages with *intentionally* unsound static type systems?
-
-
Replying to @wcrichton
Does TypeScript count? https://www.typescriptlang.org/docs/handbook/type-compatibility.html … says things like "The places where TypeScript allows unsound behavior were carefully considered", which sounds like what you're looking for.
1 reply 0 retweets 12 likes -
Replying to @qualmist
Will Crichton Retweeted Will Crichton
It does, although I'm realizing "sound" is hard to characterize. In a PLT sense, Typescript statics + dynamics are collectively sound b/c anything not caught by type system is checked at runtime. No stuck states / UB / segfaults / etc.https://twitter.com/wcrichton/status/1285700061712785408 …
Will Crichton added,
6 replies 0 retweets 2 likes -
Replying to @wcrichton
I can't quite see how a segfault is different (in practice) from "undefined is not a function". Is it caught-by-OS vs. caught-by-interpreter that you are noting here?
2 replies 0 retweets 0 likes -
Replying to @qualmist
Putting the PL theory hat on... If Javascript had a formal language semantics, "Undefined is not a function" would be listed as a rule. If C had a formal language semantics, *NULL would not be listed as a rule, i.e. have no semantic meaning defining the behavior.
1 reply 1 retweet 0 likes
In practice, we define *some* kind of semantics for UB, often punted to a different computation layer (e.g. the OS). But from a PL design perspective, it's important to know whether a program can enter a state for there's no official semantics.
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.
cognitive psychology. PhD