Static Typing comes in two flavors:

1. Promises from the programmer to the compiler. These allow the compiler to generate better machine code by avoiding having to check for things that the programmer promises not to do.

2. Restrictions from one programmer to another. These allow a library author to stop a library user from calling their functions with data that they aren't able to handle. (Enforced by the compiler, of course.)

Follow

Now the controversial part.

1 is obsolete. Modern language runtimes can use internal typing, speculation, and side exits to automatically make the speed improvements with no loss of generality.

2 is still valuable.

Languages with type systems designed for 1 are trying to figure out how to enable 2 without breaking backwards compatibility.

(Languages without a full runtime are in a very bad position here.)

@WomanCorn Some of us still hack on kernels, where your program *is* the runtime.

As usenix.org/system/files/1311_0 puts it,
"if you find yourself drinking a martini and writing programs in garbage-collected, object-oriented Esperanto, be aware that the only reason that the Esperanto runtime works is because there are systems people who have exchanged any hope of losing their virginity for the exciting opportunity to think about hex numbers"

@WomanCorn

Sparse is a great way to extend the C type system; sure, it's no ML type calculus, but it gives us a lot of the things we need (e.g. __user pointers, endian annotations).

Sign in to participate in the conversation
Mastodon

a Schelling point for those who seek one