I feel like your answer to “Why do we need formalizations for engineering?” just restates the claim rather than arguing for it. It sounds like you are saying ”...we need formalizations because we need gears-level understanding, and formalizations are the way you get gears-level understanding in this domain.” But why are formalizations the way to gears-level understanding in this domain? There are plenty of domains where one can have gears-level understanding without formalization.
Now, gears-level understanding need not involve formal mathematics in general. But for the sorts of things I’m talking about here (like modularity or good generalization or information compression in evolved/trained systems), gears-level understanding mostly looks like mathematical proofs, or at least informal mathematical arguments. A gears-level answer to the question “Why does modularity show up in evolved systems?”, for instance, should have the same rough shape as a proof that modularity shows up in some broad class of evolved systems (for some reasonably-general formalization of “modularity” and “evolution”). It should tell us what the necessary conditions are, and explain why those conditions are necessary in such a way that we can modify the argument to handle different kinds of conditions without restarting from scratch.
Maybe I’m just not interpreting “same rough shape” loosely enough. If pretty much any reasonable argument counts as the same rough shape as a proof, then I take back what I said.
I basically agree with this if we’re viewing this post as a standalone. I only had so much space to recursively unpack things, and I figure that the claim will make more sense if people go read a few of the posts on gears-level models and then think for themselves a bit about how what gears-level models look like for questions like “why does modularity show up in evolved/trained systems?”.
When I say “same rough shape as a proof”, I don’t necessarily mean any reasonable-sounding argument; the key is that we want arguments with enough precision that we can map out the boundaries of their necessary conditions, and enough internal structure to adapt them to particular situations or new models without having to start over from scratch. In short, it’s about the ability to tell exactly when the argument applies, and to apply the argument in many ways and in many places.
I feel like your answer to “Why do we need formalizations for engineering?” just restates the claim rather than arguing for it. It sounds like you are saying ”...we need formalizations because we need gears-level understanding, and formalizations are the way you get gears-level understanding in this domain.” But why are formalizations the way to gears-level understanding in this domain? There are plenty of domains where one can have gears-level understanding without formalization.
Maybe I’m just not interpreting “same rough shape” loosely enough. If pretty much any reasonable argument counts as the same rough shape as a proof, then I take back what I said.
I basically agree with this if we’re viewing this post as a standalone. I only had so much space to recursively unpack things, and I figure that the claim will make more sense if people go read a few of the posts on gears-level models and then think for themselves a bit about how what gears-level models look like for questions like “why does modularity show up in evolved/trained systems?”.
When I say “same rough shape as a proof”, I don’t necessarily mean any reasonable-sounding argument; the key is that we want arguments with enough precision that we can map out the boundaries of their necessary conditions, and enough internal structure to adapt them to particular situations or new models without having to start over from scratch. In short, it’s about the ability to tell exactly when the argument applies, and to apply the argument in many ways and in many places.