>>3formal proof is a pipe dream for most real-world software. to prove something, you need to formally specify it, and this is not trivial - constantly changing (e.g.
ENTERPRISE) or difficult to define in objective terms (e.g. vidya) requirements are one thing, another is 'unknown unknowns' (e.g. maybe you have proven that your program correctly implements an algorithm - but that's not the only thing that can go wrong with software; security is the other, and because there are many different exploitation techniques, you can't just implement a single catch-all rule like 'it's not possible to write past the end of a buffer' and say that you've proven your program secure). so your 'real programmers' are mostly just the followers of the current academic fad