[rudenoise]

Can anyone comment on how this implementation of TLS compares to the recent ocaml/mirageOS version?

How much does formal verification matter/increase confidence?

Is the rust version easier to integrate with other stacks?

https://mirage.io/blog/why-ocaml-tls

[hannob]

Neither ocaml-tls nor this new one do formal verification. The only TLS library that does so is miTLS.

[nickpsecurity]

Let's not forget the security kernel in Guttman's cryptlib. It's like a lightweight variant of formal verification that justs makes sure things interface correctly.

[strmpnk]

Which is interating here since F* can extract to OCaml. I wonder how hard it would be to wire up a test harness to compare the two with randomized tests.

[jeffdavis]

OCaml has more runtime requirements. Can someone comment on how invasive those requirements are, and whether that would limit adoption of the OCaml version compared with C or rust?

[edraferi]

Is that still true in MirageOS, which runs as a Unikernel on top of Xen?