Lean4 is a fascinating language because it is both a general purpose programming language and a proof assistant (like Ada, Coq, Idris, etc). It’s gaining a lot of adoption in mathematics through its Mathlib with prominent figures like Terence Tao formalizing his textbook in Lean4 (analysis | Reservoir). Google Deepmind has also been working with Lean4 and Mathlib (GitHub - google-deepmind/formal-conjectures: A collection of formalized statements of conjectures in Lean.).
It’s a functional language that also has dependent types (types as a first class language object, like how functional languages have functions as first class language objects), allowing for expressing specific constraints at compile time that would otherwise result in runtime errors, such as a function that only takes vectors of length 3.
I’m of the opinion that with the advent of LLMs writing code, formal verification of software will become more accessible and more mainstream. With that, Lean4 would be a natural choice since the codebase and the verification can be written in the same language.