>ported a small fluid dynamics simulation program from C++20 to Haskell, Lean 4 [...]
Interesting seeing L4 be used for general programming. Others worth mentioning are:
1. Idris. General-purpose language but also proof assistant (~L4). It has few back-ends incl. C, JS, and JVM, so quite a large span of usable domains.
2. Glean. Rust-like syntax/UX, runs on Erlang VM, simple tooling (all-in-one compiler, build tool, fmt, pkg manager). Very modern-looking overall.