TimeZoneDefault (12.02.2016 17:18, просмотров: 1) ответил Evgeny_CD на Спасибо! Да, у них там есть хаскельный код в репозитории, и какой-то кодогенаратор на их собственном DSL. Все это весьма близко к подходам, которые я здесь много лет ковыряю. А именно - программист пишет не "сразу в С", а в некий DSL, который, в
последний тезис упирается в понятие "обратимых вычислений", которые существуют не для всех классов алгебр. для алгебры чёрча - формально не существуют :) поэтому большие дядьки ломанулись в экзотику квантовых компьютеров.
вот и обоснование:
digitalphysics.ru/pdf/Benev_P--Kvantovo_mehanicheskaya_gamiltonova_model_mashiny_Tyuringa.pdf
на самом деле это обоснование только углубляет проблему - накладывает жёсткое ограничение на гамильтониан системы(д.б. const(t))
тов.Непейвода опубликовал очень эмоциональную статью,
2012.nscf.ru/Tesis/Nepeivoda.pdf
которая подтверждает необходимость специализации получаемой таким образом машины Тьюринга.
"В терминах битов,
чисел и последовательного исполнения в этой области работать не получится."
поэтому работы по верификации и проекты по верификации в нынешнем виде - не более чем разговоры из оперы "ишшо одна звёздочка у старой гостиницы". лестницы, диваны, бл@ди и уборщицы остались те же.
)