Conversation

swann
@evertedsphere
Make haste slowly, with abstract specs and expressive typing
Quote Tweet
Hillel
@hillelogram
·
Replying to @themattchan
This is how the seL4 people did it. They wrote an abstract spec, then translated that into Haskell, then translated the Haskell into C. They said the C translation took just 3 week, compared to original Haskell refinement taking 2 years. According to them it saved a lot of time.
1
13
Hillel
@hillelogram
On the other hand, it took them 3 person years to prove the C actually matched the Haskell. So make haste a _little_ faster than the seL4 team :P
1
3
Toby Murray
@tobycmurray
Next/current steps include: QuickCheck, networking code, IoT, extending cogent for security reasoning (not just correctness). Ping me if curious more
2
3