I'm going to try Lean4. It's interesting for us at work, for gamedev, and I'm personally interested in it too.

It's not only a programming language, but also a theorem prover, and the boundaries between those two aspects are rather blurry. For instance, if does not take a Boolean as argument, but a Decideable logical proposition. if also does not only choose which branch to evaluate, but also offers a proof that the proposition is True or False in the respective branches, that one can later use to argue with the compiler if a certain function call is allowed or not (for instance, one can make a type that only contains natural numbers that are prime - and making an instance of that type requires a proof that the passed in number is indeed prime - and such a proof can be materialized using if).

I'm still learning the language though, and am not certain if I can finish reading the book Functional Progrmaming in Lean till AoC starts... If I can't manage, I'm just going to start AoC in Lean anyhow, and see how far I get.