|
|
|
|
|
by LightMachine
1197 days ago
|
|
It managed to write, in one shot, a working λ-calculus parser, using a very specific programming style I asked it in JavaScript, and then translated it all to Python, including sarcastic, rhyming GLaDOS comments. https://twitter.com/VictorTaelin/status/1635726202231988225 It also seems to be extremely competent at writing Agda types and proofs. We need some tool that highly integrates it with entire codebases, allowing for major refactors to be requested as a prompt. That would be groundbreaking (understatement of the year), specially if coupled with a strongly typed language that prevents it from accidentally breaking things up. |
|