3 ms·

F-star, which was used to build a verified TLS implementation. https://fstar-lang.org/ https://fstar-lang.org/ Though I guess that's actually on the far side of

• hyperbrainer 2y ago
  The full language is indeed even further ahead of Rust on the spectrum I am looking at, but this seems like a cool effort. I love proof-based languages and dependent types, so this is an absolute win. 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#the-essence-of-low https://fstarlang.github.io/lowstar/html/Introduction.html#t...