This year, we published a paper "Engineering with Logic: Rigorous Test-Oracle Specification
and Validation for TCP/IP and the Sockets API" in the Journal of the ACM! :) so glad that this is finally out :D (happy to hear your thoughts on that, still working on a TCP/IP stack based on that work)

and now, thanks for nothing, I'm actually going through the specification (384 pages, typeset HOL4 code with lots of comments) and the source (there are more internal notes and comments) to come up with an actual implementation (in a pure functional subset of some programming language)... pretty interesting what my brain comes up in respect to things that are not needed (in certain environments -- such as "process of this socket no longer exists" -- which can't happen in a unikernel)... :D

@hannesm you’re also published the MirageOS paper recently? Develolping with functors ?
@hannesm oh that’s annoying. IIRC this is the only one major paper on mirageos?
Sign in to participate in the conversation

Server run by the main developers of the project 🐘 It is not focused on any particular niche interest - everyone is welcome as long as you follow our code of conduct!