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.
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.
Depends on the application. I would personally use Rust for embedded applications (since it’s low-overhead and ADTs are basically a requirement for safe parsers) and Haskell for non-embedded. But if neither of those float your boat, there are other safe-by-construction parser-friendly languages available, mostly from the ML family.
