I am interested in the convergence of AI-generated code and programs-as-proofs: can I work together with AI using a language with a highly expressive type syste

I am interested in the convergence of AI-generated code and programs-as-proofs: can I work together with AI using a language with a highly expressive type system such that we co-develop a specification in types and properties, then co-develop the implementations that fit the specification. It's not practical to do that sort of thing alone, as there's a lot of tedious nonsense involved. Maybe it will be more practical with an AI assistant. Whether current AIs are more or less somewhat close to the basics of how humans might be approaching code writing is more of a philosophical point, but a "translation room" view of the human mind might on occasion make me feel like I'm just working off patterns from my data sets. :-)