3 ms·

I don't technically have a horse in the unikernel race but have only been following the MirageOS team. From what I understand unikernels or "operating system a

I don't technically have a horse in the unikernel race but have only been following the MirageOS team. From what I understand unikernels or "operating system as a library," are not not a new idea. The cost of implementing an entire TCP/IP stack for every unikernel ecosystem is probably what kept them from being adopted early on. However we have some good specifications these days and battle-hardened implementations to test new ideas against. I think the idea behind MirageOS is that they see C/glibc/etc as a liability. So building a TCP/IP stack in a pure-functional language is an interesting idea. Just because we have a reliable system now doesn't mean we can't make it more robust by experimenting with new ideas. One certainly needs to take more care building unikernel infrastructure than a typical web application or script. I'd only touch them in production with verifiable formal specifications and a strongly-typed functional language implementation... but that's light-years ahead of what a typical gnu/linux VM guarantees. (Also the reason why I don't think size will matter here is that they all aim to be pretty small and in a cloud, 42KB difference on HVs with >64GB of RAM doesn't make much of a difference)

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 ago
  Probably... 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/

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 ago
Probably... 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/