| |||
|
|
Существует компилятор некоторого C-подобного языка, сертифицированный (он написан на proof assistant-е Coq, а тот устроен так, что все программы, написанные на нём, грубо говоря, содержат доказательство своей корректности). Компилирует для PowerPC, а оттуда уже думаю несложно построить трансляцию в машину Тьюринга и доказать её корректность. http://pauillac.inria.fr/~xleroy/pu Добавить комментарий: |
||||