Comments 42
Очень сложно читать статью, потому что вместо текста — списки-списки, бесконечные списки.
в трети мест список хорошо бы превратить в текст, в трети — написать через запятую. Оставшуюся треть можно оставить. Например, в «Устойчивость к входным данным» первый список из одного пункта — это просто ух!
Точно. Нечаянно переключил редактор в Маркдаун режим и без единой правки все поехало. Так лучше?
А разве Oberon это не мертвый академический язык? Как можно говорить о безопасности инструмента, который не тестировался на реальных проектах?
Ну вот тут можно взглянуть на применения.

Среди прочего управление беспилотными ЛА, расчет фазированной антенны для радара Еврофайтера, моделирование в физике высоких энергий.
То, что академики сразу после компилятора зафигачили себе ОСь — среду разработки — Word Pad — подобием ActiveX в одном флаконе и всё это в 1988 году — это, разумеется, семечки, а не реальный проект.
UFO landed and left these words here
Чтобы он был промышленным, нужен хороший компилятор и стандартная библиотека. И с тем и с тем у АО большие проблемы
UFO landed and left these words here
рекурсию запретить.

Смело


Иметь защиту от обращений… в чужое адресное пространство.

Встроено в каждую современную ОС


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

Heartbleed передаёт привет, лол

Встроено в каждую современную ОС
  1. не везде они современные
  2. не везде даже есть ОС
  3. ОС плевать что ты делаешь со своими потокам
Heartbleed передаёт привет, лол
Логи то читать все же надо, и править. А вот крешить программу зря — не надо.
Очень, очень советую посмотреть Rust. Это первый индустриальный (не академический) универсальный язык (т.е. от веб-фреймворков до модулей ядра), у которого вместо Си-подобной модели языка «язык позволяет сделать, а пользователь думает как не ошибиться», применяется другая: «язык старается не допустить ошибок, а пользователь думает, как бы сделать».
А, я понял. Вам нужен язык, в котором гарантировано нет ошибок, зависаний и т.д. Такой язык есть, и он работает с скоростью машинного кода. Называется eBPF, встроен во все ядра линукса уже несколько лет.

Как он работает? Программа на eBPF проверяется, если она подходит, то ядро загружает не eBPF, а результат его компиляции в машинные коды (очень быстрые).

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

Подробнее про eBPF: lwn.net/Articles/740157
Почитал, но из этого краткого введения не понял несколько вещей, может, подскажете?
1. Не совсем понял про sanity checks
The second stage is more involved and requires the verifier to simulate the execution of the eBPF program one instruction at a time. The virtual machine state is checked before and after the execution of every instruction to ensure that register and stack state are valid.
В рантайме проверяется состояние кждый раз, или единожды на этапе компиляции?
2. Возможно ли работать с eBFP без ОС? Иначе говоря, перейти от 10 виртуальных регистров и интерпретации к реальным 8/32битным регистрам аппаратуры?
verifier проверяет программу перед тем, как «принять» (загрузить) её в ядро. Он симулирует исполнение и смотрит, не попортили ли стек и регистры.

К регистрам аппаратуры, наверное, перейти можно, но после этого никто не может гарантировать адекватность вашей программы. Вдруг, вы dma-контроллер перепрограммируете чтобы всё перезатереть.
Насколько «проверяет»? Полная проверка подразумевает конечное число состояний, что требует достаточно сильного допущения о однопоточности и гранулярности общения песочницы с ядром. А МК (в статье речь в первую очередь о них) не нужен без периферии, т.е. без асинхронности: даже если по переполнению таймера, считающего на частоте ядра, читать его значение, то оно будет от 6 до 14 в зависимости от модели, компилятора и качества кода. eBPF поможет избавиться от зависания и зацикливания, но вот использовать его при асинхронности и модификации глобального состояния…
Начал читать, там про всякие узкоспециальные сетевые применения, не очень понятно можно ли его применить для чего-то кроме этих задач.
Там история возникновения. Сначала это был «packet filter» для сетевиков. Потом его начали использовать для трассировки приложений. Сейчас это почти универсальная lightinig speed виртуальная машина в ядре, которая гарантирует, что программа не зависнет в бесконечном цикле (и не попортит всё вокруг) перед тем, как её запускать.
Может напишете пост о том как напрогать какую-нибудь консольную утилиту на нём?
Там еще и есть слово unsafe. Но только вот для реальной жизни ничего лучше нет.
Ну тогда остается идрис или агда с проверкой тотальности всех функций.
А вышеупомянутые языки предоставляют какие-то специальные инструменты для гарантии того что функция тотальная?
Да, там есть totality checker. Консервативный, но не всесильный: для некоторых функций приходится постараться, чтобы объяснить тотальность. А, скажем, как изложить известное мне доказательство тотальности интерпретатора просто типизированного лямбда-исчисления, я совсем не знаю.
См последний абзац перед дисклеймерами. Вполне можно и Раст прогнать через прокрустово ложе _всех_ требований.
Отсутствие рекурсии — необязательное требование? ( ADA )
Аналогично — сборка мусора? ( Active Oberon )

Итого: стоит добавить в список Modula-3
( да и Modula-2 стандарта ISO )
Насколько я в курсе, идеального языка не существует =)

Так что ничего абсолютно обязательного быть не может, но какой то критерий конечно важнее.
ничего абсолютно обязательного быть не может, но какой то критерий конечно важнее
А не использовать ли нам «плечи титанов»?
Например, «список некоторых ограничений, вводимых SPARK» для того, что бы мы могли применять инструментарий формальной верификации:

  1. Все выражения (в том числе вызовы функций) не производят побочных эффектов. Хотя функции в Ада 2012 могут иметь параметры с режимом in out и out, в SPARK это запрещено. Функции не могут изменять глобальные переменные. Эти ограничения помогают гарантировать, что компилятор волен выбирать любой порядок вычисления выражений и подчеркивают различие между процедурами, чья задача изменять состояние системы, и функциями, которые лишь анализируют это состояние.
  2. Совмещение имен (aliasing) запрещается. Например, нельзя передавать в процедуру глобальный объект при помощи out или in out параметр, если она обращается к нему напрямую. Это ограничение делает результат работы более прозрачным и позволяет убедиться, что компилятор волен выбрать любой способ передачи параметра (по значению или по ссылке).
  3. Инструкция goto запрещена. Это ограничение облегчает статический анализ.
  4. Использование контролируемых типов запрещено. Контролируемые типы приводят к неявным вызовам подпрограмм, генерируемых компилятором. Отсутствие исходного кода для этих конструкций затрудняет использование формальных методов.

Спарк это уже более жесткие ограничения. Пока остановимся на Аде.
Но с идеей, что какую то особо ответственную часть программы/системы можно писать с более жестким контролем (ака СПАРК), а часть — с послаблениями (Ада), я согласен.

Аналогично с формальной верификацией — не везде ее применение стоит свеч.

Вы только что описали требования к ответственным или встраиваемым программам, исполняемым в жестком или мягком реальном или времени. Все уже изобретено: Codesys, IEC61131-3, Matlab Simulink, Embedded Coder

А остальные программы недостойны стабильной и быстрой работы и разработки?

Мягкое реальное время это как осетрина второй свежести. Не нужно злоупотреблять этим термином, да и я же не внес РТ в перечень требований.

Codesys — редкое поделие (в сравнении, конечно), но вот если была аналогичная среда для разработки прикладных приложений — было бы неплохо. Это одна из идей для 2й части статьи.
А остальные программы недостойны стабильной и быстрой работы и разработки?

Да, но вы не забывайте, что подход к проектированию таких программ и требования будут совершенно неадекватными. Например такая вещь, как динамическое выделение памяти. В программах реального времени статическое выделение памяти — это Маст хев. Но представьте себе Firefox выделяющий себе при запуске память под все. Я думаю ему и 16ГБ не хватит. Windows с определенной реакцией на события? Приготовьтесь, что на стандартном процессоре 3,0 Ггц это будет в пределах 2с, но зато всегда и везде. Это хорошо?


Не нужно злоупотреблять этим термином, да и я же не внес РТ в перечень требований.

Вы написали, что требуете определенного времени обработки данных — это одно из требований для программ, исполняемым в реальном времени.

Я писал, что статическое выделение памяти возможно только для определенного класса программ.

Откуда такие данные про замедление до 2с?
Ни в каких тестах не наблюдал даже 10-кратного замедления от проверок.

Для человека время реакции программы 100-200мс — вполне достаточно, если говорить о прикладной области.
Откуда такие данные про замедление до 2с?
Про FF не уверен, но если уменьшим free RAM до 3Gb ( например, стартовав 1-2 VM Hyper-V) и откроем побольше окон в IE, то получим нечто похожее
Для человека время реакции программы 100-200мс — вполне достаточно, если говорить о прикладной области.

Недостаточно. Если машина каждый клик будет обрабатывать по 100 мс, пользователь выкинет её в окно через пять минут.
Реакция программы — это отработать все действия и выдать результат. Например, отрисовать другое окно по клику.

VS вот переход на новую страницу в мэйл.ру на сайте, за ~1с уже раздражает.

Ну пожалуйста — действие — запустить программу. Длительность выполнения может достигать и 5с и выше. Это комфортно? Думаю не очень, но нард придумывает что-то. Критично? Вряд ли.
А как вы можете ускорить это, с вашим подходом?

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

Впрочем об ускорении этого см.мои предыдущие публикации.
Общая идея понятна, но детали требуют уточнения.

Из уже описанного (только где есть что возразить или уточнить):

> использоваться регистронезависимые имена.

Наоборот, это путь к диверсиям типа «пытался вызвать X, а подключило x». Что различается внешне для человека — должно различаться и внутренне. Эта проблема доказана неоднократно, и все современные языки тяготеют таки к различению регистра (вряд ли вы найдёте за последние 10-20 лет такого, где регистр игнорируется). Если не хотите проблем с этим — явно форсируйте один регистр для всех. Да, например, имена будут выглядеть в духе createtransaction, CREATE_TRANSACTION. Значит, вам так надо.

> должна проводится жесткая проверка видимости переменных и функций. Опечатавшись, можно использовать идентификатор из более общей области видимости, вместо нужного

Содержание этой «жёсткой проверки» непонятно. Не допускать перекрытия вообще? Это плохой метод, тогда можно получить поломку, например, от обновления библиотеки. Требовать явного импорта всего во внешнем окружении во внутреннее? Годится для отдельной функции, но очень быстро задолбёт в блоке, в котором всего лишь введена пара своих новых переменных. Хотя тут можно, наоборот, потребовать явной пометки «да, я делаю переменную с таким же именем, как во внешнем блоке».

> не допускаем одинаково именовать разные сущности — если есть константа с таким названием, то не должно быть одноименной переменной или имени типа

Правило избыточно, и специфично для C-like языков, в которых конфликт имён переменных/функций/etc. и имён типов это последствия синтаксиса в духе «TimeKeeper time_keeper(Timer());» В синтаксисе, в котором эти проблемы изначально устранены (Pascal, Ada, Go...), тут не больше вреда, чем в одноимённых переменных index в соседних функциях.

> крайне желательно, именование проверять по всем модулям проекта — легко перепутать, особенно если разные модули пишут разные люди

Не надо тут ничего «проверять», это работать не будет. Одинаковые имена в разных местах — нормально. Нужно, чтобы импорты были явными.

> Должен быть определенный порядок вызовов функций. При записи X = funcA() + fB() или Fn(funcA(), fB(), callC()) — надо понимать, что человек рассчитывает получить вычисления в записанном порядке, (VS) а не как себе надумал оптимизатор.

Это, как и для элементов выражения, слишком жёсткое правило, проверено на Java, где такое установлено всегда. Да, как и во многих похожих правилах, ~90% случаев такое позволяют без заметной потери производительности или утолщения сгенерированного кода. Но для оставшихся нужно разрешать компилятору переупорядочение и вообще больше свободы.

> Исключить похожие операторы. А не как в С: + ++, < <<, | ||, & &&, = ==

С тут, согласен, некоторые чрезмерны и вообще требуют перевода на слова.
Случай с = и == вообще тяжёлый вариант, но тут мне нравится больше другой подход — дополнительная пометка, что значение присвоения будет использоваться.
Тогда: if (a = b()) — не пройдёт компиляцию; нужно if (take a = b()).

> Желательно иметь немного понятных операторов и с очевидным приоритетом. Привет от тернарного оператора.

Вот тут не понял, тернарный как раз очень понятен. Есть тонкость в понятии его «приоритета», но тоже нечасто даёт проблемы. Хотя можно, конечно, установить, что его части только с более высоким приоритетом, тем самым потребовав скобок на все вложенные использования.

> Переопределение операторов скорее вредно. Вы пишете i := 2, но (VS) на самом деле это вызывает неявное создание объекта, для которого не хватает памяти, а диск дает сбой при сваппинге и ваш спутник падает на Марс :-(

Смешаны две (или три?) совершенно разные вещи.
Против переопределения в целом — это вопрос используемых библиотек, но часто оно нужно и важно. Вон есть комплексные числа, кватернионы, матрицы-векторы и т.п. Без пользовательских типов и их переопределений придётся всё писать на вызовах функций и процедур, а это плохо оптимизируется, плохо читается и т.п.
В языках, где переопределение не допускается (Go), есть предложения ввести те же комплексные числа, кватернионы, матрицы на уровень языка. Но это же изврат, по любому ;(

Для сравнения, в Ada, который специально разрабатывался под надёжность, такие переопределения есть. Значит, они не так страшны.

А память — это вторая тема. Это я писал ещё 20 лет назад, но воз и ныне там. Рецепт считаю по-прежнему самым надёжным и актуальным: обеспечить каждой задаче управляемый ею резерв памяти, автоматически подключаемой при недостатке, и этот резерв должен обеспечиваться ОС на всех уровнях (вплоть до swap area). Тогда она сможет обеспечить себе такой резерв, какой нужен.

> Нужна инициализация всех переменных дефолтными значениями.

Вот тут настолько согласен, что явно это скажу ;) Давно уже компиляторы достаточно умны, чтобы выкинуть эту инициализацию, если она не нужна.
Опять же, можно синтаксическим контекстом выключать это, но зачем?

> нужен контроль за размерностями присваиваемых объектов — защита от затирания памяти, арифметическим переполнением типа 65535+1, потерями точности и значимости при приведении типов, исключение сравнения несравнимого — ведь целое 2 не равно 2.0 в общем случае.

> И даже типовое деление на 0 может давать вполне определенный +INF, вместо ошибки — нужно точное определение результата.

Для надёжного языка требуется реакция по умолчанию на переполнение — генерация ошибки, а если кому-то надо иначе — пусть задаст явно (типом операции, синтаксическим контекстом). Вы говорили про систему типов, но сейчас это обычно реализуется не типами, а свойствами самих операций — как &+ в Swift, overflowing_add() и т.п. в Rust. В Ada, да, типы, и случаи всяких счётчиков уходят в «type Byte = modulo 2**8» и т.п.

Сюда же — методы реакции на такие случаи, как
— деление на 0 (как минимум, не должно быть «мы не знаем, что будет, но какая-то ошибка уровня ОС»)
— сдвиги в общем с выносом не-нулей за пределы целевого типа (должно быть два сдвига влево — один как умножение на степень двойки, а другой как для битового поля; и это не зависит от беззнаковости сдвигаемого)
— сдвиги на ширину целевого типа и больше (бывает, что они таки нужны, и надо это уметь реализовывать; а по умолчанию — вызывать ошибку)

Приведение типов — упоминалось, но в случае 2 и 2.0 я считаю, что вообще автоконверсия не для констант должна быть запрещена, а явная конверсия должна уточнять метод округления, реакцию на переполнение, неточную конверсию. Это касается и int<->real, и int<->int, и real<->real (разных размеров). Integer promotion, как в C, C++, должен быть отменён.

Управление памятью — да, тут нужно что-то в стиле C#, Rust: творишь странное — явно помечай unsafe.

> Программа должна работать на любых входных данных и желательно, примерно одинаковое время. (VS) Привет Андроиду с реакцией на кнопку трубки от 0.2с до 5с; хорошо, что не Андроид управляет автомобильной ABS.

А это вообще, как правило, не вопрос языка, это вопрос написания кода на нём и построения рантайма.
И рассматривать его надо в терминах realtime: общий тип (hard/firm/soft), гарантированное время реакции с разной вероятностью (90/95/99/100%), ограничение уровня потерь, измеренных как значение целевой функции.
Да, можно вспомнить исполнения GC с непредсказуемым временем, но торможение Android по кнопке питания — явно не GC.

> Например, программа должна корректно обрабатывать и 1Кб данных и 1Тб, не исчерпав ресурсы системы.

И снова, это не вопрос языка. Если программа всосала все данные в состояние процесса одним read(), то чем язык виноват?
А вот какая-то помощь в диагностике таких некорректных подходов, да, может быть оказана и языком.

> Очень желательно иметь в ЯП RAII и надежную и однозначную обработка ошибок, не приводящую к побочным эффектам (утечкам ресурсов, например). (VS) Очень веселая вещь — утечка хендлов, проявиться может через многие месяцы.

А тут никакой язык, боюсь, не поможет до конца. Просто надо писать с пониманием обстановки. Можно и на Rust сделать кольцо из ARC-ссылок, и в чём он будет виноват?
Да, есть некоторые типовые проблемы языков с AMM — что там не вызывается Dispose/finalize/etc. вовремя, если это явно не гарантировать своим кодом. Но на сейчас нет, по-моему, однозначно надёжного решения этого вопроса в принципе, все варианты управления памятью и ресурсами страдают по-своему.

> Было бы неплохо защититься от переполнения стека — рекурсию запретить.

В общем случае — нельзя. Рекурсия полезна. А вот сделать возможность защищаться от рекурсии на конкретных выбранных функциях — да, полезно. И статически (помечать часть функций таким образом), и динамически при исполнении (хоть это и дорого).

> Устойчивость к многопоточной работе — защита приватных данных потока, и механизмы гарантированного обмена между потоками. Программа в 200 потоков может работать совсем не так, как в два.

Первое — в принципе вопрос того же memory management. Второе — вопрос удобства механизмов синхронизации. Например, каналы очень помогают там, где не нужна высокая компактность данных.

> Программа должна целиком загружаться в память — без подгрузки модулей, особенно удаленно.

Вообще исключать DLL//SO — очень часто слишком дорого, местами и невозможно. Вообще, надо давать возможность такого ограничения, но всегда требовать — перебор. Ошибка загрузки всё-таки хорошо ловится на уровне выше.

> Очищаем память при освобождении (а не только выделении)

Очень дорого. По умолчанию не должно включаться (да оно и при выделении не включается, если это не память от чужих задач). По явному запросу — да, сейчас делается везде (для секьюрити).

Чего не увидел или увидел иначе:

2. В обсуждении знаков операций (operators), не сказано более важное: грамотные приоритеты и ассоциативность.
Правила C — когда, например. сдвиги менее приоритетны, чем умножения, и выражение a + b >> c понимается как (a + b) >> c — диверсия, потому что даёт систематические ошибки.
Пример исправления — в Swift: они вынесены на уровень умножения и деления, где им и место.
Аналогично с другими операциями — например, & должно быть с умножением, | — со сложением.
Сравнения не должны быть ассоциативны! a == b < c — не должно парситься. Кому надо — только с дополнительными скобками.

Должно быть управление режимом алиасинга, «дружественным» по умолчанию к программисту (пусть и в ущерб эффективности), то есть компилятор не должен предполагать, что разные указатели (или как это будет выглядеть в языке) указывают в разные места. Где программист согласен на такое — должен явно уточнять.

Вообще же самое сложное на сейчас — это правильный баланс между стилями управления памятью (ручной, счётчики ссылок, GC...) и обеспечение корректности работы в каждом. В хорошем языке могут использоваться все три, но выбрать режим для каждого, а особенно правильную реализацию их стыка — это задача ой нетривиальная.
Only those users with full accounts are able to leave comments. Log in, please.