it looks less like “move everyone to Haskell and Coq” and more like “design a good core-library crypto API for X” and “reform common practices around npm”.
+1, coq is my dayjob and I’m constantly telling people to be less messianic when they talk about formal verification.
by designing the APIs so that doing things the safe way is easy, and doing things the dangerous way requires calling functions with “dangerous” in the name
+1, want to extend it by paraphrasing the ancient folk wisdom that I think comes in flavors for both libraries and languages: “things are bad when good behavior is impossible, things are good when bad behavior is impossible, everything comes in a spectrum of easier or harder bad or good behavior”, which can be read in terms of rewards and punishments (easy code is rewarding, hard code is punishing).
+1, coq is my dayjob and I’m constantly telling people to be less messianic when they talk about formal verification.
+1, want to extend it by paraphrasing the ancient folk wisdom that I think comes in flavors for both libraries and languages: “things are bad when good behavior is impossible, things are good when bad behavior is impossible, everything comes in a spectrum of easier or harder bad or good behavior”, which can be read in terms of rewards and punishments (easy code is rewarding, hard code is punishing).