История изменений
Исправление red75prim, (текущая версия) :
Согласно соответствию Карри-Говарда [...]
Всё это здорово, но ещё есть Blum size theorem: длина программы на total programming language (язык, который гарантирует существование результата вычислений для любых входных данных) может превосходить длину программы на обычном языке в любое количество раз. https://existentialtype.wordpress.com/2014/03/20/old-neglected-theorems-are-s...
Поменяется спецификация немного и окажется, что нужно дописать несколько квадриллионов строк. Так что какой-то баланс между корректностью и практичностью всё-таки необходим.
Исходная версия red75prim, :
Согласно соответствию Карри-Говарда [...]
Всё это здорово, но ещё есть Blum Size theorem: длина программы на total programming language (язык, который гарантирует существование результата вычислений для любых входных данных) может превосходить длину программы на обычном языке в любое количество раз. https://existentialtype.wordpress.com/2014/03/20/old-neglected-theorems-are-s...
Поменяется спецификация немного и окажется, что нужно дописать несколько квадриллионов строк. Так что какой-то баланс между корректностью и практичностью всё-таки необходим.