> I'd like to read people treating languages and platforms as tools and not as cargo cults. You don't read carpenters writing they'll ditch hammers for screwdrivers because the old cupboard they are fixing uses nails. You read carpenters debating the pros and cons of using hammers versus screwdrivers. And you read better carpenters that debate how cupboards are designed, because it is ultimately more important than whether they are glued, nailed or screwed.
The problem with this carpenter analogy is that it simply doesn't scale - a carpenter is not going to build a skyscraper. To build skyscrapers we need engineering - the practical application of science - something which is completely missing from our field. We call ourselves software engineers, but we're really software masons - we can do good work in small quantities, but we're terrible and building big structures - which is where many of our software problems lie.
You can't build a house on some land, and later turn it into a skyscraper either - because the foundations are perhaps the most vital part of the structure - they need to be designed with some knowledge of the size, shape and mass of the structure they intend to support. The approach taken in software development is the tacking on of new systems - building structures equivalent to say, the Kowloon walled city (unsightly and unstable).
To do engineering and science, we need math - and we have no sound way of modeling imperative languages/programs in ways that makes them useful as mathematical concepts. FP is math - so building up concepts in these languages is providing a richer set of math objects and abstractions which we can later use to build our large structures. Using FP doesn't mean we need to abandon imperative coding - it just means we should clearly mark the effects of such imperative chunks of code, so we can treat them mathematically.
Carpenters are still relevant in the construction of skyscrapers - but their responsibilities are only a small part of it - they're given clearly defined boundaries of when and where they should be working. This is really how we should be doing software - we need engineers and architects to build structures, using science and math, then assigning isolated environments for the "masons" (e.g, junior programmers) to work in - in such a way that a mistake by a junior programmer cannot bring the entire skyscraper crashing down. (Turns out this was understood in the 70s, because Unix pipes and processes are still the best approach we have to this day).
Of course, this doesn't mean it should be "my Coq is better than your Twelf" - we need to separate the math from the textual representations and even the execution models.
I think your post mostly re-enforces the OP's claim that FP won't save the day. To quote the OP, "it is obvious to me that doing FP right is (and will be) very hard."
In-so-far as your claims are true and germane to FP, they merely re-enforce this critique. After all, doing math right is very hard.
> and we have no sound way of modeling imperative languages/programs in ways that makes them useful as mathematical concepts.
This simply isn't true. There exist sound logics of imperative programs, which can be used to explore mathematical concepts.
This also pre-supposes that imperative programs themselves (and machine models more generally) are not an interesting mathematical concept.
> FP is math
It's entirely unclear what this means, if anything. You probably mean to say that certain functional languages correspond to certain logics. But that's not terribly meaningful; you can establish similar correspondences with imperative languages.
And even then, logic is math does not imply that math is (just) logic. So even if you're granted this point, the rest of your argument doesn't follow.
From a more empirical perspective, plenty of mathematicians do great math without knowing anything about FP, and plenty of FP programmers write a ton of code without ever doing interesting math.
Finally, the vast majority of very mathematically informed programming is still done in languages like C and Python and Java. So I'm highly suspicious of the claim that we need programming languages which are close to foundations in order to do mathematically informed programming.
The problem with this carpenter analogy is that it simply doesn't scale - a carpenter is not going to build a skyscraper. To build skyscrapers we need engineering - the practical application of science - something which is completely missing from our field. We call ourselves software engineers, but we're really software masons - we can do good work in small quantities, but we're terrible and building big structures - which is where many of our software problems lie.
You can't build a house on some land, and later turn it into a skyscraper either - because the foundations are perhaps the most vital part of the structure - they need to be designed with some knowledge of the size, shape and mass of the structure they intend to support. The approach taken in software development is the tacking on of new systems - building structures equivalent to say, the Kowloon walled city (unsightly and unstable).
To do engineering and science, we need math - and we have no sound way of modeling imperative languages/programs in ways that makes them useful as mathematical concepts. FP is math - so building up concepts in these languages is providing a richer set of math objects and abstractions which we can later use to build our large structures. Using FP doesn't mean we need to abandon imperative coding - it just means we should clearly mark the effects of such imperative chunks of code, so we can treat them mathematically.
Carpenters are still relevant in the construction of skyscrapers - but their responsibilities are only a small part of it - they're given clearly defined boundaries of when and where they should be working. This is really how we should be doing software - we need engineers and architects to build structures, using science and math, then assigning isolated environments for the "masons" (e.g, junior programmers) to work in - in such a way that a mistake by a junior programmer cannot bring the entire skyscraper crashing down. (Turns out this was understood in the 70s, because Unix pipes and processes are still the best approach we have to this day).
Of course, this doesn't mean it should be "my Coq is better than your Twelf" - we need to separate the math from the textual representations and even the execution models.