[smasher164]

I think it's a good time to learn Lean. It positions itself as a proof assistant that's also good at practical programming. I'm not sure how mature the ecosystem is for the latter.