For the same reason not all software is written in Coq/Agda/other proof systems: it would be incredibly expensive, slow, and demand very rare skills.
For the same reason not all software is written in Coq/Agda/other proof systems: it would be incredibly expensive, slow, and demand very rare skills.