I think Lean is another closely related language. It is very famous for its theorem proving capabilities, of course, but it seems that it can also express effec

I think Lean is another closely related language. It is very famous for its theorem proving capabilities, of course, but it seems that it can also express effectful computations (aka, real world programs). Somebody managed to solve Advent of Code with Lean: https://github.com/anurudhp/aoc2022 https://github.com/anurudhp/aoc2022 Somebody managed to write a raytracer with Lean: https://github.com/kmill/lean4-raytracer https://github.com/kmill/lean4-raytracer