Proving correctness means proving one to one correspondence between models and solutions.
Theorems like splitting set and generalizations are useful for proving correctness.
For devising translations maybe a few ideas are needed. These ideas should be used as idioms. One example is completeness:
Are these intuitively correct? With these idioms in mind high-level languages work.
Implementations of high-level languages are important to test bigger examples!