Provable correctness means you have to model your source and target languages. And then translate the source model to the target model. It is theoretically possible, but in practice, modeling an industry language is way too much work. Some languages do not even have a spec :/