Hi Irwan,Short answer: yes I agree. (and noting that Coq changed name to Rocq recently)Thinking more deeply, I like their description of a continuum from accessible, low complexity methods to full automated proofs. Model checking - which is usually how TLA+ is used - is on their diagram, and it's also not the simplest technique. Calling out that the simplest thing is to just write more tests (up to some point of saturation) is an interesting reality check when considering the value of any formal methods type work.I think integrating TLA+ with other techniques and having modeling interact well with other engineering processes is good. For instance, linking testing with a TLA+ model, like we've been doing with trace validation recently, is nice. It means your new TLA+ model might be checked against implementation code in CI, and the client could be reminded that the model exists whenever they break the validation step. I'm sure other things could add this type of value too.I was actually at a presentation of this idea a few months ago by coincidence, and that's the sort of impression it left on me.Best,-Finn--On Sun, Jul 13, 2025 at 12:51 AM Irwansyah Irwansyah <irwansyah@xxxxxxxxx> wrote:Hi Finn,In my understanding, the company is using Coq and not TLA+ and both have different concerns, right? TLA+ is less on math and proof while Coq is heavy on math and proof. So if the company is using TLA+ shouldn't the project be way more cheaper than using Coq?Irwan--On Sun, Jul 13, 2025 at 2:07 PM Finn Hackett <fhackett.py@xxxxxxxxx> wrote:Someone recently reminded me of this article, and I think it adds to conversation about contracts here. Maybe some of the learnings are applicable. https://www.galois.com/articles/what-works-and-doesnt-selling-formal-methods--I know at least one other person here saw this already, but maybe not everyone.Best,-Finn
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CAJs285nvmYE-pkMU65FMg6QOz5H8gvY0CSa%2B7%3DzA9imUj7xpbA%40mail.gmail.com.
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CA%2BKOs4yC%2BoPBYUxM97zmAV_wBrU5V4qDkcdw_Mh%3D%2BxwzCD89vg%40mail.gmail.com.
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CAJs285kx56GC_5BbaLjST33evZNmRXhKYkCaxiPHaQHxm5izWg%40mail.gmail.com.