It seems anecdotally that there's a boom in formal proof languages. The posts on HN usually link to someone's in-progress repo "this language will aim to prove..." as in they are unfinished.

I am guessing there's an awakening coming from functional languages that mathematical proofs can help with code verification. Do you have an explanation if this is a phenomenon, what benefits there are, examples, etc?