[Haskell-cafe] Well typed OS

[Barak A. Pearlmutter]

At a high level, you seem to be proposing encoding and enforcing
safety properties of executables using a type system. One
instantiation of this idea is proof-carrying-code (Necula and Lee,
1996, see https://en.wikipedia.org/wiki/Proof-carrying_code), which
ensures safety properties of machine code. The spin-off Cedilla
Systems built a mobile OS (intended for phones) around this, with the
idea that third-party apps would run unprotected with safety
guaranteed solely by sophisticated use of types. The Fox Project,
http://www.cs.cmu.edu/~fox/, was philosophically similar, and their
web page contains a bunch of interesting pointers to relevant work.

For whatever reason, this stuff never got much penetration. But in
today's Internet of Things, with malware being injected into mobile
phones and cars and light bulbs and toothbrushes and smart dust, it
may deserve another look.