4 ms·
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 le
by ozten 4y ago
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 4y agoI 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.