[Haskell-cafe] Well typed OS

[Barak A. Pearlmutter]

> I would guess a factor that prevented something like PCC from taking off is the fact that proofs over binaries are relatively pretty challenging to express and verify, and ISA semantics tend to be really complicated.

The Cedilla folks had a pretty clever way of dealing with that issue.
They had a very small proof checker on the embedded device, which used
highly compressed information associated with the binary to basically
guide a theorem prover, where the information helped the prover make
all its choices.

This information was generated from a proof generated by a compiler,
which compiled a high-level language (C in their case) annotated with
extra safety-proof-related information down to both machine code an a
proof of that machine code's safety. So they sort of did what you're
describing, but partially evaluated away the IR.