Skip to main content
3 events
when toggle format what by license comment
Jul 5, 2016 at 5:13 comment added Artelius Your answer suggests that the 'automated proof system' reviewed L4's source code automatically. Actually it reviewed a human-written proof of L4's correctness. The proof took years to complete. Nonetheless there is a lot to learn from this endeavour about how to write correct code. (To be clear, this isn't a pen-and-paper proof but a machine-readable proof that actually 'imports' the entire source code and reasons about it. See ssrg.nicta.com.au/publications/nictaabstracts/3783.pdf)
Jul 1, 2016 at 16:42 history edited Cort Ammon CC BY-SA 3.0
added 646 characters in body
Jul 1, 2016 at 16:23 history answered Cort Ammon CC BY-SA 3.0