[nickpsecurity]

Ada with SPARK Ada variant and careful refcounting wouldve been my baseline given it's all safe by default before Rust came along. D also had potential. Now Rust with SPARK. Im keepimg SPARK in for semi-automated verification. Just rewriting Skein's C code in SPARK automatically found an error thanks to prover. If affording specialists, then something like F star used in miTLS verified stack, Isabelle/HOL, Jasmin language, and/or imperative ML. All core, trusted functionality done that way.

I choose languages with tight control on memory for crypto-related stuff since you want to prevent leaks. You'll follow with a covert-channel analysis to be sure. If not crypto and stopping code injection, then a memory-safe language with interface checks and input validation will cover most problems. Those have been around since one was deployed in first, business mainframe: Burroughs B5000.

[hiq]

What do you mean by imperative ML? Using a language from the ML family, but mostly its imperative features? Can you expand on that?

[nickpsecurity]

Yeah, I should have. There's been prior work porting linear types and other stuff (think Rust safety) like that to ML since that's an easy-to-analyze language academics like to work in. Tolmach et al actually made a converter for it to Ada one time. ML is also the language that most formal verification extracts to by default. CakeML is a verified compiler for ML. There's flow analysis and concurrent variants for it. So, ML by itself is a good choice for correct code that will get a lot of analysis. Imperative ML, imperative for the needed efficiency gains, combined with type systems like Rust's to ensure its safety with numbers mapped to say 64-bit can go a long way.

When I wrote it, though, I was mainly thinking of recent work that converts functional, verified specs into imperative specs that extracts to ML. I think that has a lot of potential for producing a pile of verified data structures with low cost similarly to the COGENT language that was used for ext2 filesystem. Got a link for Imperative/HOL-to-ML below.

http://www.ssrg.ece.vt.edu/~lammich/pub/itp15_sepref.pdf

[zerokernel]

I didn't expect anything interesting to come up as replies, but here we are - thanks for those insights.