For a very simplistic example, say I ask for a trusted program that can add up all of my expenses. The person who writes the spec than defines this as `add_expenses xs = reduce - xs`. They then prove that write a program that matches this specification. The program will be "bug free" in the sense that it will perfectly match this spec. But it will certainly not be what I asked for - so from my point of view, it would be an extremely buggy program.
For a more subtle example, consider encryption algorithms. It's generally fairly easy to specify the encryption scheme, and then check that a program implements that exact algorithm. And yet, it's very likely that a program built only to such a spec will actually leak secrets through various side-channels in practice (either key-dependent timing or even key-dependent CPU usage, and others). Again, it would be fair both to say that the implementation is bug-free (it perfectly matches the spec) and that it is deeply buggy (it doesn't actually protect your secrets).
> I feel that massive effort is being misdirected because of some fundamental misunderstandings
The misunderstanding here is with them and what they're looking at. The author doesn't discuss business problems, but lists this as a motivation in their "basic" summary:
> Category theory is a powerful and highly-general branch of mathematics, which is applied for all kinds of purposes. It has been formalized in several existing proof assistants, but only as a result of a ton of difficult work. The type system of (1,1)-directed type theory is specifically optimized for category theory; it manages to automate a lot of the difficult "bureaucracy" of formalizing category-theoretic results, so it doesn't require as much work.
i.e. it makes certain proofs easier.
The system also will only allow that proof to be used for the proposition you have declared so even if you somehow declared the wrong thing and proved it without realising, that wouldn’t affect the consistency of the system at all.
Reading mathematical sentences (types, basically) is like step one in maturing from baby to toddler in math.
To whom? Fully formalized mathematics is extremely dense and difficult, and few mathematicians actually practice it, especially for complex problems. Just because the symbols are theoretically unambiguous doesn't mean that any human can actually understand what they mean, and whether they accurately encode some less formal system you were hoping to study.
And this becomes much more problematic once you go from the realm of pure mathematics into other realms, like engineering or economics or anything else that is seeking to model real-world phenomena. A model can be perfectly self-consistent and still be a very bad and even useless model of a real-world thing. And it can be highly non-trivial to figure out to which extent and under what constraint a model actually matches the phenomenon you intended.
For examples of both kinds of issues, look at theoretical physics. Lots of major physics theories are only partly formalized, and rely on unproven or sometimes even known to be unsound mathematical foundations (like the Dirac delta at the time it was first introduced, or like renormalization in quantum physics). And, of course, there are still open questions on how well these theories actually model various physical phenomena (like GR and black hole curvature singularities).
This doesn't work for everyone though; some people find it easier to stay grounded in specific models.
Since Lean code isn't the same as natural language or even unobservable human intention, there might always be a mismatch between what the author of a Lean proof claims (or believes) it proves, and what it actually proves.
Like if you have some f:R->R, a:R in context and write ∀ϵ>0,∃δ>0 s.t. x: R, |x−a|<δ ⟹ |f(x)−f(a)|<ϵ, no one is confused about what you mean.
If you instead write ∃δ>0 s.t. ∀ϵ>0 x: R, |x−a|<δ ⟹ |f(x)−f(a)|<ϵ, you've written something different. Everyone in the field knows this, and actually it's even more obvious when you look at types in something like Lean: roughly ϵ -> (δ, h) vs. (δ, ϵ->h).