Perhaps my followers don't need to hear this, but sometimes I see troubling myopia among FP people about formal methods. Formal methods is a much broader field than just proof assistants and type theory. There is so much interesting stuff out there.
Conversation
Also you can do formal methods about imperative code! Separation logic, for example.
1
3
Formal methods on imperative code predates formal methods on functional code.
2
6