Maybe this can give a boost for languages like idris or F*, where you can specify much stronger types than in normal languages (with the price that you might ha

Maybe this can give a boost for languages like idris or F*, where you can specify much stronger types than in normal languages (with the price that you might have too proove the types manually). The types can help "tame" the AI generated code, and the AI can help generate the proofs. I also wonder if it could be useful in creating Coq proofs!