News for hackers. Stuff that matters.

A comment on L4 microkernels: The lessons from 20 years of research and deployment. Parent comment

Re:L4 microkernels: The lessons from 20 years of research an... by hughw on Tuesday September 20, 2016 @01:42PM (#12541422)
Where does one go to learn these formal methods?
[ Parent | on HN ]
Re:L4 microkernels: The lessons from 20 years of research an... by cmrx64 on Tuesday September 20, 2016 @01:54PM (#12541584)
Depends on what level of detail you're interested in. You could check out ADA/Spark or Dafny. Or, investigate something like Isabelle/HOL or Coq - perhaps via http://concrete-semantics.org/ or http://adam.chlipala.net/cpdt/.
[ Parent | on HN ]
Re:L4 microkernels: The lessons from 20 years of research an... by elihu on Tuesday September 20, 2016 @01:50PM (#12541535)
I'm not very knowledgeable in this area and haven't used these tools myself, but you could start by looking into theorem-proving tools like coq and agda.
[ Parent | on HN ]