3 ms·
It's true that unikernels, if done right, give you the possibility of formal verification. So that would be a definite selling point for MirageOS as opposed to
by cheez 11y ago
It's true that unikernels, if done right, give you the possibility of formal verification. So that would be a definite selling point for MirageOS as opposed to IncludeOS. Can they do it, though?
- agentultra 11y agoProbably... many of the people behind MirageOS are Cambridge-educated people. I have no university degree and I'm picking up TLA+ as my first foray into formal methods quite well. The amazing thing is that for correctness the maths behind TLA+ is really easy to understand. I think many people involved in systems-level programming could pick it up with just a couple of weeks' training. I don't think they have done it though... which makes reading through their TLS implementation rather difficult, IMO. The type system of OCaml will give some guarantees but it has a hard time catching high-level design errors that TLA+ and formal methods will. update This also doesn't preclude them, or anyone with an interest, in creating specifications for these systems. Amazon started using formal methods and found bugs in several AWS services after the fact. update update s/SSL/TLS/