“Theorem proofing” may be beside the point (and it is a different can of worms). But regarding this question:
why we can not complete source with intentions or needed knowlegde and derive implemenations for each programming language?
This is basically modifying the original language to extend it with annotations that explicitly describe the intent of the code (“this for loop that contains an ‘if’ is actually a collection partial traversal applying this predicate”, “this pointer here is actually a child-parent reference”, “this enumeration is actually a state machine”). You may also want to forbid using constructs and features that are too implementation oriented and harder to map. You are in effect creating a higher level programming language, one that uses (possibly a subset of) the original language but is much easier to translate to the intermediate language.
Yup, that is totally possible, but you are no longer supporting programs in the original language (most existing code would not be supported). No problem with that, as long as you keep that in mind.
I have been exploring that approach myself using Kotlin+Spring Boot as a source language for model-driven business applications. See this example - that is the entire source of a business application, complete with a functional backend, database persistence, a REST API and a generic UI. The abundance of annotations is hard to miss. You can notice the presence of mechanisms that need to be used to complement the base language, such as a state machine implementation, annotations to describe relationships, entities, query operations so on and so forth, concepts that are part of a more abstract language and lack in the base language.