История изменений
Исправление firkax, (текущая версия) :
Разворачиваю мысль: верифицировать алгоритм обычно обозначает переписать его на другом, сухом и строгом, математическом языке. Что для такой сложной программы как компилятор может быть просто неподъёмной задачей.
У тебя просто будут баги в ходе конвертации ТЗ, написанного бытовым языком, в этот самый «сухой и строгий» язык. То есть алгоритм на «сухом и строгом языке» в бинарник у тебя превратится корректно и ты будешь уверен, что бинарник соответствует тому что ему подали на вход, но вот сам по себе алгоритм будет не тот что хотел заказчик. Собственно, при обычном программировании на Си происходит ровно то же самое: компилятор полностью корректно превращает твою писанину в бинарник, проблема в том что писанина расходится с желаниями (в т.ч. теми которые вообще нигде не сформулированы иногда). Изначально строго сформулированная задача есть только у уже упомянутых числодробилок. Как вы не поймёте, что проблема вообще не в том месте где вы её представляете.
Ещё как в курсе. Зачем вы мешаете всё в одну кучу и теорию и практику.
Вот вот, есть бесполезные теоретики-графоманы и есть полезная практика. Я как раз намекал что стоит смотреть на второе.
Исходная версия firkax, :
Разворачиваю мысль: верифицировать алгоритм обычно обозначает переписать его на другом, сухом и строгом, математическом языке. Что для такой сложной программы как компилятор может быть просто неподъёмной задачей.
У тебя просто будут баги в ходе конвертации ТЗ, написанного бытовым языком, в этот самый «сухой и строгий» язык. То есть алгоритм на «сухом и строгом языке» в бинарник у тебя превратится корректно и ты будешь уверен, что бинарник соответствует тому что ему подали на вход, но вот сам по себе алгоритм будет не тот что хотел заказчик. Собственно, при обычном программировании на Си происходит ровно то же самое: компилятор полностью корректно превращает твою писанину в бинарник, проблема в том что писанина расходится с желаниями (в т.ч. теми которые вообще нигде не сформулированы иногда). Как вы не поймёте, что проблема вообще не в том месте где вы её представляете.
Ещё как в курсе. Зачем вы мешаете всё в одну кучу и теорию и практику.
Вот вот, есть бесполезные теоретики-графоманы и есть полезная практика. Я как раз намекал что стоит смотреть на второе.