> It's uncommon in industry, currently, because it is hard and most programs don't need to be reliable. But, if it were easy to guarantee correct code, it's som

> It's uncommon in industry, currently, because it is hard and most programs don't need to be reliable. But, if it were easy to guarantee correct code, it's something that everyone would want. Well, the sort of obvious reason we don't / can't formally validate most programs is that we don't have a rigorous, complete, consistent description of what the program is supposed to do.