Re: [tlaplus] Using TLAPS for industrial stuff?

I would say this is more of a problem with deductive proofs in general -- a cost/benefit ratio that may be at odds with the constraints of most industrial systems -- rather than TLAPS in particular.

On Thursday, September 12, 2019 at 9:23:58 PM UTC+1, Stephan Merz wrote:

I am not aware of any significant use of TLAPS in industry yet, and quite frankly I don't think that it would be usable at this point for proving the correctness of any significant system. One of the problems is that it requires people to state a full inductive invariant. Of course, I'd be more than happy to be convinced of the contrary.

Stephan

On 12 Sep 2019, at 10:28, Thomas Gebert <thomas...@xxxxxxxxx> wrote:

This is a more generic question, but I had a bit of trouble finding concrete answers on this.

You can find a bunch of examples of industry usage of people using TLA+ with TLC to verify their designs, and that's really cool, but it made me wonder; does anyone know of any examples of using the proof system for that? Is this a silly question?

--
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 tla...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/52189418-0691-4252-b43d-94a86782676d%40googlegroups.com.