[leovonl]

> And I can actually not remember a single time when this was actually useful [..]

This tells a lot about what is wrong with software development and why industry is constantly plagued with security issues, misbehaving systems, buggy behaviour on edge-cases, etc.

There was a thread on HN some time ago about software engineering, and I remember mentioning that if "software engineering" was really to be taken seriously, we'd be using theorem proving to guarantee software is correct.

The best analogy is the bricklayer vs structural engineer: you can build something simple very quickly without really putting too much thought about soundness, but once you go past a few floors the risks are too big to be ignored - which is why we have the latter.

It usually boils down to cost - some people like to spread the idea that formal methods are sorcery or are limited in scope, specially people outside of computer science that have no strong background on mathematical methods, which sometimes do a disservice to the efforts of researchers and the ones that had exposure to the theoretical foundations of CS.

In any case, I don't want to go on a huge rant here - so if you don't know, it doesn't hurt to spend some time reading about modern tools and applications for this, maybe even playing with available tools, and.. who knows, maybe learn something new.