Выбор языка программирования для систем высокой целостности

Question

Какие языки программирования являются хорошим выбором для систем высокой целостности?

Примером плохого выбора является Java, так как существует значительное количество кода, недоступного для программиста. Я ищу примеры строго типизированных блочно-структурированных языков, где программист отвечает за 100% кода, и как можно меньше мешает таким вещам, как JVM.

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

EDIT: Системы высокой целостности - это общий термин для систем, критичных для безопасности и т. Д., Безопасных систем и т. Д.

РЕДАКТИРОВАТЬ РЕДАКТИРОВАТЬ: Мне нужны примеры языков, на которые не влияет платформа, которые будут давать одинаковый результат независимо от компилятора и полностью определены.

Answer 1

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

SPARK можно использовать без времени выполнения. Аналогично для языка Ада (см. Прагму No_Runtime).

Конечно, с такими языками, как SPARK, вы торгуете гибкостью ради безопасности (или безопасности).

Answer 2

Какую высокую интеграцию вы ищете?

• Галуа в Портленде, штат Орегон, создали очень успешный бизнес на системах с высокой степенью целостности, написанных на Haskell . Я считаю, что они подчеркивают целостность данных и безопасность. Несколько удивительно делать такую ​​работу на таком сложном языке, с очень сложной системой времени выполнения, но система типов Haskell предоставляет очень строгие гарантии, а семантика языка обеспечивает гораздо более строгие принципы рассуждения, чем большинство языков. Кроме того, вы, как правило, пишете гораздо меньше кода для каждого приложения, поэтому его легко показать правильным.

• Если вам нужны еще более строгие гарантии, SPARK Ada (или просто SPARK в наши дни) - это относительно простой, традиционный императивный язык, который поставляется с полной формальной семантикой и инструментами для полной формальной проверки. Вы получаете более надежные гарантии, чем с Haskell, но по более высокой цене, как в капитале, так и в труде.

Answer 3

Я думаю, что ADA обычно используется для этого.

Answer 4

Возможно, вы захотите подумать в терминах Eiffel , где более строгое соблюдение предварительных и постусловий облегчает системы высокой целостности.

Answer 5

Я не до конца понимаю, что это за система с высокой степенью целостности. Предполагая, что вы имеете в виду «систему, которая оставляет меньше места для ошибок», я предлагаю вам взглянуть на ML и его производную ООП O'CaML . ML был разработан, чтобы минимизировать ошибки типа. В ML нет ошибок приведения или нулевых указателей - вы просто не можете их кодировать. В нем также отсутствуют динамические функции - что делает его менее крутым, но более безопасным.

Сказав это, ML далеко не восхищение хакеров; Это несколько громоздкий язык. Но если вы предпочитаете работать на час больше и получать на одно исключение меньше, это подходящий выбор.

Answer 6

Это противоречие в терминах. Строго типизированные блочно-структурированные языки почти всегда компилируются компилятором, создавая машинный код, за который программист не несет ответственности Если вы хотите быть на 100% ответственным за код, вам нужно использовать язык ассемблера.

Answer 7

Вы можете искать то, что хотите, но не получите.

Ваши требования не совместимы друг с другом. Они в основном полностью исключают любую библиотеку. Вы можете сказать, что можете использовать C / C ++ - но БЕЗ КАКИХ-ЛИБО ФАЙЛОВ И СТАНДАРТНЫХ БИБЛИОТЕК (за которые программист, очевидно, не несет ответственности).

Это оставляет вас в значительной степени на суше - требование нереально. Даже с большой командой никто не захочет перепрограммировать большинство библиотек.

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