Hacker News new | ask | show | jobs
by SwellJoe 3206 days ago
Most interesting to me is that it's implemented in a language I'd never heard of, F* (https://www.fstar-lang.org/), which is an ML that compiles to OCaml, F#, or a subset of the language can compile to C. It's intended for just this sort of work ("verified effectful programming" is seemingly one of their taglines for the thing).

That's pretty neat. I like seeing exotic languages used in mainstream projects. It's just fun, ya know? Firefox is also shipping with some Rust code these days.
2 comments
dsacco 3206 days ago
F* is somewhat well known in circles of information security, but it's not widely used in general. It's frequently used for formal verification of cryptographic protocols. If you look at the papers on the website you'll see a variety of applications for provable security in crypto.

I wouldn't call it a general purpose language (in the sense that you can productively use it for just about anything), but to be fair I've only read papers about/using the language; I've not used it personally. It's a great leap forward for provable security in general, though.

link
fmap 3206 days ago
F* is a great project and under very active development. Basically at every POPL you find papers with genuine improvements and simplifications to the core of F*. I don't know of any other language that's improving this rapidly.
link