It always boils down to use-cases. Ultimately, what formal verification gives you is a guarantee of structural correctness, but not behavioural correctness. Wh

It always boils down to use-cases. Ultimately, what formal verification gives you is a guarantee of structural correctness, but not behavioural correctness. Whether a program behaves as intended or required is still a task for humans. Garbage in - garbage out. Whether structural correctness is a requirement is a function of the software's criticality and purpose. You probably don't need it for your blog... There is one critical FYI. If you require formal verification of your code you have to give up Turing-completeness. https://en.wikipedia.org/wiki/Total_functional_programming https://en.wikipedia.org/wiki/Total_functional_programming