Здравствуйте, mihoshi, Вы писали:

M>Технология доказательств эквивалентности или других свойств алгоритмов уже давно существует. Это одно из основных приложений декларативнрого программирования. Например, доказательство корректности qsort я видел своими глазами Разумеется, это происходит не полностью автоматически (кроме совсем простых случаев) — надо все-таки формально описать алгоритм доказательства. См., например, http://coq.inria.fr/

Да, я знаю о таких разработках. В приницпе, сам читал в какой-то книжке доказательство корректности программы вычисляющей факториал средствами исчисления программ Хоара и Флойда (аксиоматическая семантика). Однако ход рассуждений там, на сколько я представляю, не алгоритмтизирован. Т.е. процесс доказательства во многом творческий (что, кстати, видимо лишний раз подтверждает идеи Тьюринга).

А за ссылочку большое спасибо