This is true in the sense that such a proof can't have "implementation bugs". But it can very much still have "specification bugs", where the formal specification doesn't actually match the fuzzy intention of whoever asked for the work.

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).

None of this has anything to do with proof assistants. What you're saying is mathematical modeling doesn't perfectly capture real world phenomena. Everyone knows this. It also has nothing to do with proof assistants. The statement I was replying to was

> 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.

A formal proof really can’t have a specification bug. You say in the declaration what proposition you intend to prove and if you succeed in instantiating that type then you have succeeded in your proof.

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.