One the whole, we do. But sometimes abstractions leak [1]. Sometimes you get impedance mismatches when you try to layer them. Sometimes the abstraction isn't what you think it is or want it to be.
An example of the last point is alluded to in a comment by efaref about a binary search algorithm that turned-out to be broken because it assumed that an integer type in the implementation language behaved the same way as integers in mathematics, but it didn't because it didn't allow arbitrary-size values. The abstraction provided by the integer type was faulty.
If one were using formal methods in these circumstances, they should, in principle, reveal those leaks and impedance mismatches to you (or, more precisely, reveal to you any problems they cause in your specific design.) The existence of leaks and impedance matches in informal abstractions is an argument for formality, not against it.
I agree in principle, although in practice I am sceptical about the practicality of applying formal methods to large systems. The ratio of effort to reward just seems too large for most domains.
One the whole, we do. But sometimes abstractions leak [1]. Sometimes you get impedance mismatches when you try to layer them. Sometimes the abstraction isn't what you think it is or want it to be.
An example of the last point is alluded to in a comment by efaref about a binary search algorithm that turned-out to be broken because it assumed that an integer type in the implementation language behaved the same way as integers in mathematics, but it didn't because it didn't allow arbitrary-size values. The abstraction provided by the integer type was faulty.
[1] https://en.wikipedia.org/wiki/Leaky_abstraction