undefined | Better HN

0 pointsstrken1y ago0 comments

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.

0 comments

VBprogrammer1y ago

It is possible that the person you replied to wasn't confused by that. I've certainly come across the type of developer who'd deride the lack of ability to formally test their code then, in the next breath, click through the happy path of their code and send it.

meoleo1y ago

TLA+ and Coq are too hard for most SAAS applications. Tried FizzBee (https://fizzbee.io/tutorials/getting-started/) and P (https://p-org.github.io/P/whatisP/)? These seems quite practical.

Coq/Rocq are obviously much harder to use, and I mostly see embedded systems engineers use them. TLA+ is somewhat easier, and being used in a number of cloud infrastructure companies (AWS, MongoDB, Confluent etc).

Obviously, if you are building a simple CRUDL app, these tools don't help at all.