Comment by touisteur

I wish I could have been paid to work on SPARK specification around io_uring so that one could have built on it. Or to work on SPARK-to-eBPF (there's already a llvm backend for gnat) and have some form of guarantees at the seams... alas.