So I think that's true as far as it goes, but vastly overstates how much difference fully constructive types actually make. Starting to use types, even nominal ones, to express your requirements is a real game changer, a step change in your defect rate: it turns making a correct program from an intractable global problem into a compositional problem that you can reason about locally. Using constructive types is a technique that eliminates a couple of rare classes of errors. It's fine, and if you can do it cheaply (which is pretty rare in practice IME) then it's worth doing, but it's really not a major difference-maker. And I think a post like this could easily give the impression that newtypes aren't all that, so to speak, when nothing could be further from the truth.