Теоремы Гёделя имеют очень конкретный, точный смысл, понятный математикам-теоретикам.
Не думаю, что стоит их так вольно трактовать.

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

Да и как-то сравнение пейтонов с хаскелями очень странное. При чём тут хаскель и утиная типизация? Утиная типизация и какая-либо доказательность (доказательность - это обязательно какое-нибудь статическое средство, а утиная типизация - принципиальный отказ от статики)?