[tlaplus] Re: On a type of TLA+ contract

[Andres Carignano <carignanoandres@xxxxxxxxx>]

Hello Andrew, 

I'm a first year student in computer science and I work as a web programmer. Lately I've been looking into Leslie Lamport's papers and video lectures because I want to deepen my knowledge and skills in programming and mathematics. I've been wondering: what stops TLA+ from generating C style code? Is this a design decision or a technical obstacle? Maybe my question is incredibly basic, if so I apologize, my journey just begins. Maybe you can point me in the right direction.

Best regards,
Andrés Carignano.

On Friday, July 4, 2025 at 2:29:03 PM UTC-3 Andrew Helwer wrote:

Hi all,

I wrote a post on a type of TLA+ contract I've done a few times, why it never worked out as well as hoped, and what could be changed so future contracts see more success:

https://ahelwer.ca/post/2025-07-04-tla-contracts/

Andrew Helwer

-- 
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/31283a1a-c182-4aa7-ad6c-a2ea2396cdc1n%40googlegroups.com.