3 ms·

for fun, I popped it into ChatGPT o3-mini-high, had it generate the TLA+ code then compare its version to the human-written version: https://chatgpt.com/share/

• hwayne 2y ago
  I see at least a few errors with the TLA+ code: - It says that `olddb = [k \in Keys |-> CHOOSE v \in Values: TRUE]` initializes olddb nondeterministically. This is NOT true: `CHOOSE` is guaranteed to be a deterministic expression. The actual thing is `olddb \in [Keys -> Values]`. - `key \in Keys; val \in Values; newdb[key] := val;` is a syntax error. I think what it meant was `with key \in Keys, val \in Values { newdb[key] := val;` - `newdb[key] := val` is an error anyway, because `newdb` was initialized as a set. - ` for key \in DOMAIN(olddb) do` is straight up a syntax error, there's no for loop in PlusCal. - It's mixing p-syntax (`if then end if`) with c-syntax (`if {}`).
• code_monk666 2y ago
  When I wrote this, I had tried getting help from several different chat models. None of them produced anything remotely useful—but they did help me learn formal verification, as well as syntax when writing in PlusCal