The big solution I was thinking of would have to go a bit further than Python/C. Basically you should be able to write a description of the actual essential fun

The big solution I was thinking of would have to go a bit further than Python/C. Basically you should be able to write a description of the actual essential functionality of a program without going into data structure and algorithm implementation that isn't relevant to the problem domain. Something like Prolog or Haskell here, Python isn't all that declarative compared to them. Then you could write the bits that need tweaking in a lower level language, but you should be able to automatically verify that the low-level implementation matches the high-level description, at least through extensive QuickCheck-style automated testing if a full automatic proof isn't feasible. You don't get anything like this with a Python/C style solution.