personally i think you should just have a separate proof language that doesn't also try to be a programming language and build a bridge between them (ideally as a compilation target). anyways im working on this with my spare opus tokens.

yes thats the main reason, agda , coq similar ideas