eriangazag
Joined 12 years ago
Karma
85
Submissions
10
Member since
Jul 21
Recent submissions
Comment · 5 months ago
Comment · 5 months ago
(author of the post here)
Hey Maksadbek! Great question. It's a trade-off between speed of writing and trust in what you wrote, and OCaml (especially OxCaml) sits at a really good point on that curve.
Ada/SPARK has the strongest verification story and decades of space heritage, but the development cost is higher. Rust would work too, but I actively want a GC by default with the option to turn it off on the hot path. That is exactly what OxCaml's mode system gives you: zero minor GCs on the dispatch loop in the post, while the rest stays GC-managed. Haskell is great for type-driven design but its runtime cost-model is harder for low-jitter work.
Plus, the OCaml ecosystem gave me solid foundations on both fronts. For the protocol stack: MirageOS-style clean separation between wire serialisation, pure state-machine management and I/O, with ML modules and GADTs that map naturally onto protocol state machines. For the crypto: mirage-crypto for OCaml-facing primitives (fiat-crypto under the elliptic curves), and libcrux for ML-DSA-65 post-quantum signing. The CCSDS and BPv7/BPSec layers themselves I had to write from scratch (my earlier posts walk through how), and 20 years of OCaml muscle memory definitely helped!
Comment · 5 months ago
(author of the post here)
Hey Berké! I remember your talk very well (I was in the room), super interesting and it really got me thinking about this area!
Since then, the more I look into it, the more I see a fit with our MirageOS unikernel work. On the ground, you can paper over security and specialisation by throwing more machines (or money) at the problem. In orbit you cannot, so both the compile-time and the runtime guarantees have to be right!
Comment · 2 years ago
Absolutely, MirageOS is indeed pivotal in the development of unikernels. MirageOS not only developed the unikernel concept but also coined the term 'unikernel'.
MirageOS represents a significant shift in cloud and network computing, focusing on building highly specialized, secure, and efficient unikernels that streamline application deployment by shedding unnecessary components. It also puts extra focus on security, with most of the stack — including TCP and TLS — being rewritten in a type-safe language (OCaml).
Currently, MirageOS is expanding to include bare-metal and embedded systems, aiming to bring the same level of security and efficiency to this domain. The move towards embedded systems is a natural progression for MirageOS, given our emphasis on minimalism and security in environments where resources are limited and reliability is crucial. See for instance what is happening with SpaceOS: https://tarides.com/blog/2023-07-31-ocaml-in-space-welcome-s...
Comment · 3 years ago
Wasm_of_ocaml is a fork of Js_of_ocaml which compiles OCaml bytecode to WebAssembly. The generated code works with Chrome beta and node V8 canary.
Comment · 11 years ago
As for the rest of MirageOS, Irmin is a "library" database, means that you have a bunch of components than you can re-use in different contexts. Two interesting contexts are:
- the browser, where some components of Irmin are transpiled to JavaScript using js_of_ocaml (http://ocsigen.org/js_of_ocaml/). Cuekeeper (http://roscidus.com/blog/blog/2015/04/28/cuekeeper-gitting-t...) is an interesting use-case for that.
- the kernel, where some components of Irmin can be compiled into a unikernel and be run on top of Xen/baremetal, bypassing the OS completely. Irmin-ARP (http://somerandomidiot.com/blog/2015/04/24/what-a-distribute...) is an interesting step is the direction of exposing kernel data and do interesting stuff with it.
Comment · 11 years ago
Yes, you can easily add thing into a "staging area" of your database (which is hold in-memory), and then "commit" your changes to update multiple keys in one go. You can also use this mechanism to keep track of reads (what Git doesn't do) to detect read/write conflicts.
Hey dsab! I agree, but CCSDS is what we have today. We need to support it properly first if we ever want to extend or transition away. It also doesn't help that there's no good open-source implementation of the whole stack, especially the SDLS part, which makes the transition even harder.
On the type-safety side, I found typed combinators really useful for describing parsing and serialising (see my earlier post on ocaml-wire[1]), and keeping the protocol logic pure (separate from I/O) makes the whole thing much easier to test and reason about. OCaml's fuzzing support pairs really well with types too. This is basically the nqsb-TLS approach [2], which has held up in ocaml-tls for a decade.
[1] https://gazagnaire.org/blog/2026-03-31-ocaml-wire.html [2] https://www.usenix.org/conference/usenixsecurity15/technical...