There's a proof assistant now called Rocq (used to be Coq). I'm not writing about technical things here. I'm thinking about how it changed my life.

I moved from Japan to Europe twice, before and after getting a PhD in computer science. The second move to Europe was for a position in Germany that involved using Coq. If not for Coq I wouldn't be in Europe now probably.

I suddenly realized this when I was going through a lean tutorial.