I feel like this is the exact opposite of the conclusion I've been coming to. In an age where anyone can vibe code stuff at the drop of a hat, I want the ability to assert guarantees/contracts at a high level, and then let AI work out the details. I want to force AI to work within the confines of an abstraction, not independently of it.
The more semantically rich a programming language, the more it demands mathematical veracity.
The more a language is mathematically sound, the more its linguistic constructs converge to enforce same.
Programming languages which follow this path ultimately support similar capabilities; Applicatives, Functors, Monads, Monoids, and often meta-programming via higher-kinded types and/or intrinsic AST code generation.
> I want the ability to assert guarantees/contracts at a high level, and then let AI work out the details. I want to force AI to work within the confines of an abstraction,
I have the same thought on this. Having some abstraction where we have total control and we can make clear judgments is the perfect place where AI should. Removing this abstraction will just make things hard for us and just pray that all the guards around are sufficient.