What intrigues me quite a bit relative to the main topic of the HN thread is Low[0]
> Low is not only a language subset, but also a set of F* libraries that model a curated set of C features: the C memory model, stack- and heap-allocated arrays, machine integers, C string literals, and a few system-level functions from the C standard library. Writing in Low, the programmer enjoys the full power of F for proofs and specifications. At compile-time, proofs are erased, leaving only the low-level code to be compiled to C. In short: the code is low-level, but the verification is not.
[0] https://fstarlang.github.io/lowstar/html/Introduction.html#t...