What programming language will you be using in the upcoming advent of code?

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.