I’m referring to production code being good enough rather than the tooling. Let’s take HN for example. Is it coq proven? I doubt it. Is that a barrier to its s

I’m referring to production code being good enough rather than the tooling. Let’s take HN for example. Is it coq proven? I doubt it. Is that a barrier to its success?