tomthecreator

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?

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

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

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

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.

Pretty sure the "you're a liar" is just a convenient way to blow it off without going into details.

The buy was probably already questionable even for $50m, a number Steve probably already knew even before they entered the room. The exchange showed that the founders were going to be stubborn about the price.

So in the end this isn't "trust is everything in business, and Steve was offended" but simply "don't jump into negotiations with your pants down".

I'm really sorry olivdums, but it seems I cannot read your blog post because it's behind Mediums paywall. :)

Probably "invaded".