3 ms·
It will be interesting to see if the formal proof/verification work that is being done by NICTA for the seL4 project will mature into something that can be used
by reynoldsbd 11y ago
It will be interesting to see if the formal proof/verification work that is being done by NICTA for the seL4 project will mature into something that can be used practically elsewhere in industry.
https://sel4.systems/ https://sel4.systems/
- steveklabnik 11y agoYou might be interested in https://robigalia.org/ https://robigalia.org/
- cyphar 11y agoFrom my understanding, NICTA's proofs are basically algorithms to show that Haskell models and C code is equivalent. They can then go on to do proofs with their Haskell models.