Conversation

Make haste slowly, with abstract specs and expressive typing

Quote Tweet

· Jul 23, 2018

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.

Hillel

@hillelogram

Jul 23, 2018

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

Replying to

and

Yeah - one of the motivations for ts.data61.csiro.au/projects/TS/co it seems. “Given our earlier findings that verification effort scales quadratically with code size, this is key to reducing overall verification cost.” - interested to know where they are up to with this work!

3:09 AM · Jul 24, 2018Twitter Web Client