I've been using it to learn Lean, the proof assistant language, and it's great. The code doesn't always compile, but the general structure and approach is usually correct, and it helps understand different ways of doing things and the pros, cons, and subtleties of each.
From this it has me wondering if AI could increase the adoption of provably correct code. Dependent types have a reputation for being hard to work with, but with AI help, it seems like they could be a lot more tractable. Moreover, it'd be beneficial it the other direction too: the more constraints you can build into the type system of your domain model, the harder it will be for an AI to hallucinate something that breaks it. Anything that doesn't satisfy the constraints will fail to compile.
From this it has me wondering if AI could increase the adoption of provably correct code. Dependent types have a reputation for being hard to work with, but with AI help, it seems like they could be a lot more tractable. Moreover, it'd be beneficial it the other direction too: the more constraints you can build into the type system of your domain model, the harder it will be for an AI to hallucinate something that breaks it. Anything that doesn't satisfy the constraints will fail to compile.
I doubt it, but wishful thinking.