Владимир Паронджанов писал(а):
3. Из этих аксиом математически строго выводится любой слепыш (шампур-схема).
4. Слепыш (шампур-схема) представляет собой теорему, которая выводится из аксиом методом логического вывода.
5. Это означает, что слепыш не может содержать ошибок (если дракон-конструктор спроектирован правильно).
Дмитрий Дагаев писал(а):
Почему же не дать возможность Владимиру Даниеловичу попробовать доказать корректность слепышей? Хотя я, как и Алексей Донской, полностью не согласен с его утверждениями.
И я утверждаю, что найдется хотя бы одна схема, содержащая ошибки даже в слепыше, которые не распознаются предложенным исчислением икон.
Поддержу Дмитрия Дагаева, так же и Алексея Донского. И если уж говорить о строгом математическом формализме, то их правоту подтверждают теоремы Гёделя о неполноте.
Владимир Паронджанов писал(а):
Геннадий Николаевич, Вы правы. Результат будет (в строгом смысле слова) НЕКОРРЕКТНЫМ.
Но здесь корректность не нужна.
В самом первом сообщении темы я выложил пять примеров слепышей и показал результат их маршрутной трансляции. Все мои 5 примеров некорректны. Но, повторяю, здесь корректность не нужна.
Мои пять примеров представляют большой интерес.
Они наглядно показывают, что СУЩЕСТВУЕТ ПРИНЦИПИАЛЬНАЯ ВОЗМОЖНОСТЬ МАРШРУТНОЙ ТРАНСЛЯЦИИ СЛЕПЫШЕЙ.
Обратите внимание на желтые прямоугольники.
viewtopic.php?p=79978#p79978
Они указывают на НЕзаполненные места в программе.
После того как желтые прямоугольники будут заполнены (правильным) кодом, некорректная (незавершенная) программа превратится в корректную.
viewtopic.php?p=79978#p79978
Вряд ли здесь можно говорить о каком-то уровне семантической корректности программы выше, чем просто отсутствие синтаксических противоречий (хотя это тоже часть доказательства верной семантики, но только малая часть). И одного эргономичного визуального восприятия явно недостаточно, чтобы быть уверенным в корректности. Система исчисления икон далека до уровня, к примеру, темпоральной логики. Мне недавно на глаза попался документик:
Analyzing Singularity Channel Contracts. В нём небольшое описание исследования контрактов каналов для взаимодействия процессов в Singularity - экспериментальной ОС от Майкрософт. В этой операционке изолированные процессы взаимодействуют через обмен сообщениями с помощью каналов для их передачи. Каналы имеют контракты - интерфейсы, определяющие список событий, состояний, порядок отправки/приёмки сигналов и пр., которых должны строго придерживаться ничего не знающие о друг друге процессы-серверы и процессы-клиенты. У меня огромные сомнения в том, что если бы проектирование этих интерфейсов осуществлялось с помощью ДРАКОНа, то он бы наглядно показал (а в идеале - автоматически выявил бы) те косяки разработчиков (насчёт взаимоблокировок), которые определили исследователи через формальную верификацию.