Competitive Pure Functional Languages

>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.