Remix.run Logo
MarkusQ 3 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.

sdenton4 3 hours ago | parent [-]

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.

MarkusQ 14 minutes ago | parent | next [-]

> 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 of 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.

c-linkage 24 minutes ago | parent | prev [-]

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!"