You are misunderstanding and/or misrepresenting my point, which is that once enough people over a long-enough period build systems in a top-down, systematic matter, well as it works, it becomes impossible for a single person to understand a specific issue about a stack of such systems, especially once the real-world kicks in with hardware issues, bugs, and so forth, in which case you have to resort to methods that do not require keeping all relevant aspects in the head and that do not rely on the truth of idealized assumptions. Like in going from mathematics to physics, in real-world software engineering is no longer sufficient for conclusions to follow logically from the premises, since the premises now also have to be true in the real world conditions. Having non-leaky abstractions only shifts the moment in which the shift from pure thought to empiricism has to happen.
It seems to me that you actually use the notion of being "formal" in an informal (sic) way. Remember we are talking about Dijkstra-style correctness proofs and developing programs via doing mechanical in nature transformations of program invariants.
I am not convinced that in order to use the methods described one would have to keep the entire "world" in their head. In fact, I think these methods would actually help manage that problem rather than exacerbate it.
In the end a software program is and always will be an approximation of the real world.
Comments
You are misunderstanding and/or misrepresenting my point, which is that once enough people over a long-enough period build systems in a top-down, systematic matter, well as it works, it becomes impossible for a single person to understand a specific issue about a stack of such systems, especially once the real-world kicks in with hardware issues, bugs, and so forth, in which case you have to resort to methods that do not require keeping all relevant aspects in the head and that do not rely on the truth of idealized assumptions. Like in going from mathematics to physics, in real-world software engineering is no longer sufficient for conclusions to follow logically from the premises, since the premises now also have to be true in the real world conditions. Having non-leaky abstractions only shifts the moment in which the shift from pure thought to empiricism has to happen.
It seems to me that you actually use the notion of being "formal" in an informal (sic) way. Remember we are talking about Dijkstra-style correctness proofs and developing programs via doing mechanical in nature transformations of program invariants.
I am not convinced that in order to use the methods described one would have to keep the entire "world" in their head. In fact, I think these methods would actually help manage that problem rather than exacerbate it.
In the end a software program is and always will be an approximation of the real world.