3 ms·

sel4 was specified in Haskell and then converted to C

• cmrx64 10y ago
  The "real" specification (if it can be said to exist) is the abstract spec, in Isabelle/HOL.