I am not an expert, but I recently took a course on formal systems, which included theorem proving. It was more focused on proving properties for code since thi

I am not an expert, but I recently took a course on formal systems, which included theorem proving. It was more focused on proving properties for code since this is the focus of my professor, but I was really surprised how well it was working. I also recently tried out Liquid-Haskell, which adds an SMT solver (i think...) to Haskell. In my opinion, theorem proving has come a long way and I think the challenge is now equal in theorem-proving and programming language. We have to get the ergonomics right, deriving properties for imperative code is awful. We need a super elegant, easy to use and not too restrictive language that can be verified automatically. The overhead of using it must be minimal.