Comment by MarkusQ
20 hours ago
We need more of this.
For every "well of course, just...X, that's what everybody does" group-think argument there's a cogent case to be made for at least considering the alternatives. Even if you ultimately reject the alternatives and go with the crowd, you will be better off knowing the landscape.
Completely disagree; IMO we build far too many frameworks and alternatives (probably because it's fun) instead of a) enhancing the things that already exists to have the thing we want or b) just getting on with the actual work. The whole field would be much better off if we had half as many languages, half as many libraries, half as many build tools...
It depends!
Every time you go off the beaten path, you're locking yourself into less documentation, more bugs (since there's less exploration of the dark corners), and fewer people you can go to for help. If you've got 20+ choices to make, picking the standard option is the right choice on average, so you can just do it and move on. You have finite attention, so doing a research report on every dependency means you're never actually working on the core problem.
The exceptions to this are when a) it becomes apparent that the standard tool doesn't actually fit your use case, or b) the standard tool significantly overlaps the core problem you're trying to solve.
> You have finite attention, so doing a research report on every dependency means you're never actually working on the core problem.
Reading that took five minutes and gave a good intro to the counter argument to Curry-Howard-all-the-things monomania. If having invested those five minutes, Lean still seems like the way to go (for whatever reason) fine. You are making a (closer to) informed choice, and likely better off than if you'd spent those five minutes doubling down on the conventional solution.
Most deviations from the group consensus are mistakes, but all progress comes from seeing past the group consensus. So making frequent small bets on peeking around your blinders is a good strategy.
Which shows the lie of the common engineering trope "use the right tool for the job."
It really should be "use the same tool that everyone else is using so you don't have decide which tool is the right one -- the herd made that decision for you!"