forgotpwd16
2 hours ago
>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.
type-lambda
2 hours ago
Yes I was surprised how capable Lean 4 is for general programming.
I know, I have written about Idris before, but I have not used it for a while.
Glean is getting a lot of buzz, it is on my to do list. :D