Comment by andrewflnr
1 day ago
F-star, which was used to build a verified TLS implementation. https://fstar-lang.org/ Though I guess that's actually on the far side of Rust relative to what you're looking for.
1 day ago
F-star, which was used to build a verified TLS implementation. https://fstar-lang.org/ Though I guess that's actually on the far side of Rust relative to what you're looking for.
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#t...