3 ms·

afaik, the c is handwritten for performance reasons, and is manually proven to be a refinement of the executable haskell model. the haskell is then proven to be

afaik, the c is handwritten for performance reasons, and is manually proven to be a refinement of the executable haskell model. the haskell is then proven to be a refinement of an abstract, more succinct spec.

nine_k 5y ago
Fine! Now we have a way to write guaranteed safe C code. It requires quite a lot of qualification from the development team, though.
- kobebrookskC3 5y ago
  if ur fine with writing 4 lines of code a day from an expert...i guess
  - nine_k 5y ago
    With endless bug-hunting in hastily-written C code, it could be fewer than 4 lines a day of completed code. (I hope nobody actually does so poorly, except while learning C.)
    - kobebrookskC3 5y ago
      of course, with unverified code, "completed" means absence of evidence of bugs, not evidence of absence.