Personally been experimenting in Lean 4. LLMs understand it, can be given simple rules to improve it. Typing is strong, proofs are solid, and it compiles quickly.

On the contrary, for a small rust project, I had to clean out 180gb of cargo nonsense from the last ~3 days worth of compiles on a single, narrowly focused topic branch.

The library situation might be funky, but I'm also learning Lean 4 by hand. The tooling & lsp integration is lovely.