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.