OberonCore

Д.В.Дагаев (РОСАТОМ) на Дне Оберона 2017 сформулировал (в докладе, по названию которого ничего такого ожидать было нельзя) абсолютно фундаментальный принцип:

Приоритетное внимание угрозам в ущерб любым удовольствиям -- это, на самом деле, фундаментальный принцип работы центральной нервной системы, выработанный Эволюцией за 4 миллиарда лет.

Понятно, почему именно "росатомный" программист сформулировал принцип: в докладе крупно фигурировал жёлтый значок радиационной опасности:

.

И понятно, почему принцип стал актуален именно сейчас: кругом все эти беспилотные автомобили, многотонные нории, отрубающиеся системы управления воздушным движением в аэропортах и т.д. и т.п.

Принцип отлично проясняет минимализм Оберона -- такой формулировки сильно не хватало.

В докладе https://forum.oberoncore.ru/viewtopic.php?f=127&p=101972#p101972.
Новые программные продукты привносят, во-первых, новые угрозы (не верифицируемость, уязвимость к кибер-атакам), и только во-вторых, новые преимущества.
•Отсутствие обеспечение целостности при работе с указателями.
•Отсутствует изоляция данных от других задач.
•Возможность переполнения стека.
•Обеспечение LIFO-последовательности вызова сопрограмм.

Купирование последствий угроз может быть дорогостоящим (например, защита в многопоточных приложениях).

Консервативный стиль Оберона - в отказе от новомодных программных технологий (выбрасывание всего лишнего), польза от которых сомнительна, а угроза причинения вреда - реальна.

Я тут нечаянно подумал, ведь можно к программной системе применить критерий устойчивости Найквиста?
Есть вполне осязаемые метрики кода, как количественные, та и качественные.
Оберон -- про качество, код -- про количество.
Оберон -- марка стали, код -- размер щита из этой стали.
Какие будут предложения?)

Какой, к лешему, Найквист для настолько нелинейной системы?!
Каждый байт кода - потенциальная бифуркация с серьёзными последствиями.
Тут никакая метрика не даст даже качественной оценки, имхо.

Да ладно??
Использование типизированных ссылок против не типизированных никакого качества не даёт?
Или сигнатура функции по результату и параметрам ведь лучше чем просто произвольные параметры?

Коэффициент для выравнивания качества можно, скажем, предусмотреть х500. Почему нет?
А если есть аппаратная поддержка пространства модулей/кода/данных/стека -- разве это не критерий?

Само по себе - нет.
Только в комплекте с дисциплиной разработки.
На трудозатраты влияет прямо (или даже экспоненциально ), но трудозатраты и качество не взаимозависимы.

Да пожалуйста. Никто не запрещает использовать среднюю температуру по больнице.

Конечно, критерий.
Я не против критериев. Я о том, что применение Найквиста к столь сильно "устреднённым" моделям практически бессмысленно.

Вообще-то, взаимозаменяемы. Правда, я умолчу какова будет цена. Всё в этом мире имеет свою цену.

х500 -- это усреднение?))

И как же мерить качество? К примеру, вот здесь ограничений больше, чем в Оберонах (прежде всего -- статическое выделение ресурсов). Но в итоге любая программа сразу же по построению, как минимум, с гарантией отсутствия deadlock-ов и livelock-ов. И по сравнению с Обероном, к примеру, на борту имеются даже "generic"-и для обобщённых алгоритмов. Т.е. что-то урезано, но нечто другое расширено, и, главное, имеется условный формальный контроль -- вроде есть "качество", но могут быть ограничены возможности.
Но, в принципе, динамическое выделение ресурсов (включая запуск процессов) "сдерживается" лишь проблематикой верификации. Однако возможны техники частичных проверок, и если допустить "динамику" -- возможностей возникает существенно больше, и вновь под контролем.
В общем, лишь "выбрасывание всего лишнего" -- вряд ли можно принимать за фундаментальный критерий качества.

Для встроенки динамика может быть структурирована по стадиям рантайма.

viewtopic.php?f=152&t=6126

Важна также и ПРЕЗУМПЦИЯ НАЛИЧИЯ УГРОЗ.

У Дейкстры и Хоара доказывается корректность программы исходя из некоторых необходимых условий. Если условия не удовлетворяются, программа не корректна. Дейкстра говорит в идеале об "интеллектуально-управляемых программах".
Я разобрал программу по зернышкам и отдаю на экспертизу - мне отвечают, а докажите еще отсутствие взаимодействия каждого оператора одной процедуры с каждым оператором другой процедуры. Это - правильный подход.

Зато, когда речь идет о хорошем коммерческом ПО, предлагается всегда ПРЕЗУМПЦИЯ ОТСУТСТВИЯ УГРОЗ.

Я знаю, я в курсе АСУТП, но как разработчик я никаких гарантий не дам, до тех пор, пока мне не докажут каждую строчку кода.

Верификация посредством тестирования доказательством корректности не является.

Да, это должно быть явной частью Принципа.

Совершенно верно.
Можно сколько угодно тестов написать, но если память сбоит -- то код даже после верификатора будет глючить.
Доказательство трудоёмко и зачастую невозможно. Есть замечательная русская пословица:"Гладко было на бумаге да забыли про овраги"

В тех краях как раз компилятор выдаёт программы только после базовой верификации и гарантирует начальную достижимость. Здесь уточнения:
viewtopic.php?f=152&t=6126#p102120

У Мухопада были обзорчики принципов реализаций самоконтролируемых автоматов. См. в этом сборнике -- с.32:
http://docplayer.ru/39045765-Informacio ... istem.html
И ещё:
http://www.problem-info.sscc.ru/2013-1/1.pdf

Я о том, что кому нужно, тот и о железе позаботится. А верификация модели подтвердит, что все критические траектории системы правильно заданы (к примеру, не забыты спекулятивные вычисления в виде дублирования процессов, на разном железе или/и с разными алгоритмами, с последующим консенсусом -- анализ кворума результатов).

Уважаемый PVS100!))
Не считаю приличным обсуждать то, в чем половину слов не понимаю))
Академические исследования, безусловно, надо осваивать. Но освоение -- это тоже технология и к этой технологии предъявляются всё те же требования: легко понять, легко внедрить, легко поддерживать.
Шаги освоения должны быть понятными. Технология должна жизнь упрощать, а не наращивать сложность.
И не забывает про правило 80/20.

Эпиграф "Продать «смотрите, что я ради вас сделал» куда легче, чем «смотрите, от чего я ради вас уклонился»" (Нассим Талеб, Антихрупкость) подчёркивает важность формулирования оснований для отказа, в том числе на живых примерах из конкретного опыта. Про новое естественно рассказывать, а вот про отбрасываемое, ставшее не нужным, наоборот.

Пример Вирта показателен тем, что он, набирая опыт применения инструмента, создавал следующий, отбрасывая лишнее. Интересно было бы посмотреть теперь процесс с самого начала, какие "several commonly used features of other languages" не попали в Паскаль и т. д.

Не писал Вирт такого обзора?

Марвин Мински рассматривает ИИ как эмоциональную машину The Emotion Machine. §1-5. Seeing a Mind as a Cloud of Resources.

Ментальные состояния - ресурсы эмоциональной машины (нарисованные кружочками) оказываются в плену страстей: Гнев (Anger), Страх(Fear), Привязанность(Affection), Тревога(Alarm). Угроза(Threat) на рисунке рассмотрена как "смешанное чувство", захватывает ресурсы Гнева и Страха.

Если Вам хотят закрыть глаза на имеющиеся (потенциальные) угрозы в предложенном Вам продукте, правильная тактика будет в активации чувства Привязанности для притупления алармистских настроений.
- А посмотрите на наш замечательный бесплатный сыр!
- А обратите внимание на объем функций новой MS Visual Studio 2017!

В медицине этот принцип известен давно как «Не навреди», или primum non nocere

Медицинская аналогия не вцепляется в подсознание.
Может, кто-нибудь пофилософствует немного на эту тему?
Чтобы вцеплялось на уровне интуиции.