Yes. Compare also https://www.khoury.northeastern.edu/home/cmartens/Courses/74... where the abstraction itself mechanically enforces certain guarantees and contracts.

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.

formal verification? maybe theorem prover or hoare logic can come into play here.

> I want to force AI to work within the confines of an abstraction, not independently of it.

Yes, this is the way. We need programming languages that make this easier.

> 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,

Exactly right!

More details in my comment here - https://news.ycombinator.com/item?id=49269323

See also, Software Abstractions: Logic, Language, and Analysis by Daniel Jackson - https://mitpress.mit.edu/9780262528900/software-abstractions...