3 ms·
The seL4 code didn't start out as C. First they wrote the whole thing in HOL (an ML dialect), then translated that to Haskell, then translated _that_ to C. Veri
by hwayne 7y ago
The seL4 code didn't start out as C. First they wrote the whole thing in HOL (an ML dialect), then translated that to Haskell, then translated _that_ to C. Verifying code is correct is Just Plain Hard.