[ozten]

I don't know TLA+ and haven't had time to learn it. Could GPT-4 be a boon for esoteric PL that have had trouble gaining mass adoption?

Clearly, one needs to learn and understand TLA+ before one can trust generated proofs, but maybe GPT-4 could be the mentor or gentle on-ramp I was missing.

[hwayne]

I hope so! So far I've been unimpressed with ChatGPT and Copilot for generating TLA+. It mixes in idioms from other programming languages, like RETURN, which make no sense in TLA+.

What I'm hoping is that it'll be helpful for writing J. That'd be a feat.