The comment you were replying to is about formal proofs of correctness, probably using tools like Rocq (formerly Coq) and TLA+.
These tools can take an extreme amount of time to use and require specialised skillsets that are difficult to hire for. They go far beyond standard software engineering practices like unit and E2E testing. It is genuinely, seriously not practical to verify the average startup's SaaS web app with TLA+; you'd go bankrupt.
Someone who's used them more than me might be able to comment on exactly how hard it would be, but I felt it was unfair to you not to explain.
These tools can take an extreme amount of time to use and require specialised skillsets that are difficult to hire for. They go far beyond standard software engineering practices like unit and E2E testing. It is genuinely, seriously not practical to verify the average startup's SaaS web app with TLA+; you'd go bankrupt.
Someone who's used them more than me might be able to comment on exactly how hard it would be, but I felt it was unfair to you not to explain.