← Back to context

Comment by pjmlp

3 days ago

Appreciation isn't the same as market share, formal proofs in general are pretty much inexistent in enterprise, unless there are legal requirements to do otherwise.

I fail to see how you validate that TLA+ model is actually correctly mapped into the written Java code.

2 comments

pjmlp

Reply
pron  3 days ago

> formal proofs in general are pretty much inexistent in enterprise, unless there are legal requirements to do otherwise.

Formal proofs are rarely used when specifying with TLA+, too, BTW. Writing formal proofs (as you would in Lean) has a very low ROI, and even formal method fans (like me) would tell you that's a tool you should reach for very rarely, and only if you must.

> I fail to see how you validate that TLA+ model is actually correctly mapped into the written Java code.

You don't (not even with Lean), but that we can't have cars that are completely crash-proof doesn't mean that's the standard for accepting or rejecting a safety measure. With TLA+ you can make sure that the design that you have (and you can't validate is actually implemented in code with or without TLA+) is actually good.

In other words, it lets us think about design rigorously. Maybe that's not all we wish for, but it's a lot, and it's not like there are better, easier ways of doing that. Of course, if the goal is to avoid thinking hard about design, then a tool that helps us think even harder isn't what we want.