When I choose tools I like to ask "Who has the hardest version of this problem? What are they using?" I'm reaching the tipping point to adopt Nix, after seeing

When I choose tools I like to ask "Who has the hardest version of this problem? What are they using?" I'm reaching the tipping point to adopt Nix, after seeing Nix as an alternative for supporting project after project. The unstated subtext always seems to be "Nix is what the smart kids are using, but it's harder to learn." Haskell? Same religion. But the joke is that one needs a PhD in category theory to use Haskell at all, and package management has long been a Haskell sore point, yet Nix hasn't taken over. The Lean Theorem Prover? https://leanprover.github.io/lean4/doc/make/nix.html https://leanprover.github.io/lean4/doc/make/nix.html A century ago, Hilbert's program to formalize and automate mathematics was stopped in its tracks by developments in logic such as Gödel's incompleteness theorems. There is a new push involving many leading mathematicians, using the Lean theorem prover. While some imagine computers replacing people, a better model is how a chess grandmaster checks their analysis using computers. Even as the experience of observing computer Go games leads to moments of amazement, as if observing an alien tournament, the role of a human to appreciate and generalize is preserved. Primates have long used tools; our future is to coevolve with machines. Dependency hell and Gödel's incompleteness are cut of the same fabric. This is where I first read about Nix flakes.