[dsacco]

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.