Комментарий
Вообще, Шуман абсолютно прав: компьютерщики в их попытках описать мир понятным для компьютера языком придумали многие фокусы, которые аналитические философы и логики только-только начинают обсуждать. А поскольку компьютер абсолютно формален, то это "описание для компьютера" нужно доводить до полной формализации, ибо всякие недоговоренности или противоречия выскочат если не сразу, то в самый неподходящий момент демонстрации программы ее заказчику.
Вот я именно по этому раз в пару лет вожусь с высокопорядковыми логиками и прочими доказательствами. Ибо это самое передовое в том смысле, что и описание есть, и реализация тут же предусмотрена, при этом выразительность ограниченна в основном мозгами выразителя. Т.е. это какое-то хитрое сплетение теории с практике (впрочем довольно далекое от практике промышленного софтостроения, с некоторыми исключениями опять-таки).