Hacker News new | past | comments | ask | show | jobs | submit login

As far as I know, Isabelle/HOL is fairly similar to Coq, perhaps with more automation. If there is something like Software Foundations for Isabelle, I'd be slobbering all over myself in excitement to hear about it.

(And I'm still a little confused about how the C code of seL4 is verified against the formal specs. Is there something like Frama-C involved?)

Both are interactive theorem provers, so yeah. But the two school comment said Coq/dependent-types, and Isabelle/HOL is neither Coq, nor does it do dependent types :)

If you are looking for developments in Isabelle/HOL, there is the AFP: https://www.isa-afp.org/

There is also a recent book that might interest you: http://www.concrete-semantics.org/

Sweet, thanks!

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact