Rust is used a lot. Elixir/Phoenix comes up often. You’re looking for something statically typed with string guarantees and as FP as possible to make unit testing easier.

the only substantive difference I've noticed is between languages with a proof system and those without, where with a proof system is orders of magnitude better for agentic work.

In my experience, Go. It was designed to be idiot-proof. It's very verbose, not very expressive, compiles fast for quick feedback loops, strict autoformatter, plenty of examples in models' training data.

OCaml.