tomthecreator

last yeardiscuss

I’m curious about the practical workflow after you’ve written and verified a TLA+ spec. How do you go from the TLA+ proof to actual code? Is there any established process or best practices for translating the spec into implementation while ensuring you’re not introducing bugs during that translation? And once you’ve written the code, how do you maintain the connection between spec and implementation as things evolve?

tomthecreator

last yeardiscuss

There's a PDF version linked at the top of the article, it's actually much better typeset.

tomthecreator

2 years agodiscuss

I wonder the same about HN. Has anyone done this kind of analysis? Me good LLM

tomthecreator

3 years agodiscuss

To rebind it to Escape of course. :D Works wonders if you're using vim or vim mode somewhere.

tomthecreator

4 years agodiscuss

For anyone not using `merge.conflictStyle = diff3` I highly recommend trying it. It removes a lot of ambiguity when dealing with conflicting changes.

And now they introduced `zdiff3` which looks even better, will be trying it once I update.

comments