Насколько я понял тезис Черча, он эквиавалентен утверждению, что любой алгоритм в житейском смысле слова может быть записан в виде программы на языке высокого уровня.

Насколько я понимаю, написать формально доказанный компилер, скажем, с C в ассемблер MIX это вполне подъемная задача. Значительно сложнее написать доказанный компилер, который кроме корректности обладает всякими другими полезными свойствами, которые мы ждем от современного компилятора - например, выдает более-менее оптимизированный код для настоящего процессора, сравнимого по сложности с Пентиумом.