Заявленные как языки программирования с прицелом на надежность.
В алфавитном порядке — Active Oberon, Ada, BetterC, IEC 61131-3 ST, Safe-C.
Сразу дисклеймер (отмазка) — это никак не агитация “все на левый борт”, и обзор скорее академический — у языка может не быть не только активно поддерживаемой современной среды разработки, но и даже компилятора под Вашу платформу.
С другой стороны, для рассматриваемых языков есть компиляторы с открытыми исходниками, да и с нынешнем уровнем развития софтостроения — при заинтересованности, не слишком сложный синтаксис позволяет сделать личный компилятор и интегрироваться в какой нибудь Эклипс с подсветкой и парсером.
Как показатель наглядности языка, я выбрал реализацию известной многопоточной задачи Дейкстры об обедающих философах. Реализация есть в учебниках по языку и на форумах, что облегчило мне работу — осталось только адаптировать. Например недавняя хабра статья про современный С++ содержит реализацию на C++17 для сравнения.
Active Oberon (2004)
Создавался с оглядкой на опыт Паскаля, Модулы, предыдущих Оберонов с 1988г, Java, C#, Ады, а также практический опыт применения. Имеет реализацию в виде ОС A2, которая может выступать рантаймом поверх *nix или Windows. Исходники А2 и компилятора по ссылке.
Также есть проект Oberon2 to C Compiler (OOC) не привязанный к среде Оберон. Это немного другой диалект, отличия описаны ниже.
Ключевая фишка Оберона — исключительная краткость спецификации. Это 16 страниц по базовому Оберону-2 плюс 23 страницы по многопоточному Активному расширению.
Простой и понятный синтаксис, исключающий явные ошибки.
Идентификаторы регистрозависимые.
ООП с объектами на куче с автосборщиком мусора(GC).
Отличается от предшественников более привычным синтаксисом ООП в виде Экземпляр.Метод (раньше было Метод(Экземпляр)) и поддержкой многопоточности с примитивами синхронизации.
В реализации ООП нет динамической диспетчеризации, что легко может привести к ситуации — забыли дописать обработку для нового типа.
Потокам можно назначить приоритет и высоким/риалтайм они не прерываются GC. Строки в виде массивов UTF-8.
Рантайм (Система Оберон) дает интересные возможности для перезапуска сбойной процедуры/модуля/потока в случае рантайм ошибки — адресации памяти или, например, целочисленного переполнения.
Недостатком можно счесть отсутствие RAII, и удобной обработки ошибок — все через коды возврата, за исключением варианта ниже.
Оберон-2 OOC
Удобнее для экспериментов, поскольку не требует ОС Оберон — компилируется в ANSI С и нет проблем интероперабельности. Отличия от Активной версии — нет встроенной в язык многопоточности — вместо этого есть модуль работы с PThreads, зато есть UTF16, иерархическая модульность и системный модуль для работы с исключениями.
Модула-3
Есть еще родственник из немного другой ветки развития в виде Модулы-3. Создавалась на базе Оберона в противовес переусложенной Аде. Реализация тут.
По сравнению с Активным Обероном добавлены дженерики и исключения, есть библиотеки для практической работы с Юникодом, GUI, и даже Постгрессом. Упрощена интеграция с С. Другая семантика многопоточности. RAII в виде WITH (похоже на using в C#).
Но похоже, что развитие Модулы-3 остановилось в 2010 году.
Дисклеймер. Запустив WinAOS я столкнулся с TRAPами (aka abort/stacktrace или runtime error) на ровном месте — даже диспетчер задач работает с ошибками, и хотя система/рантайм и не вылетали — а только приложение, меня посетило определенное сомнение о том, что надежность определяется языком программирования =(
Также AOC является в достаточной степени замкнутой на себя, со своим подходом к разработке.
MODULE Philo;
(* Dining Philosophers Example from Active Oberon Language Report by Patrik Reali *)
(* Adapted for running in AOS by Siemargl *)
IMPORT Semaphores := Example8, Out;
CONST
NofPhilo = 5; (* number of philosophers *)
VAR
fork: ARRAY NofPhilo OF Semaphores.Semaphore;
i: LONGINT;
TYPE
Philosopher = OBJECT
VAR
first, second: LONGINT;
(* forks used by this philosopher *)
PROCEDURE & Init(id: LONGINT);
BEGIN
IF id # NofPhilo-1 THEN
first := id; second := (id+1)
ELSE
first := 0; second := NofPhilo-1
END
END Init;
PROCEDURE Think; (* Need lock console output *)
BEGIN {EXCLUSIVE}
Out.Int(first); Out.String(".... Think...."); Out.Ln;
END Think;
PROCEDURE Eat;
BEGIN {EXCLUSIVE}
Out.Int(first); Out.String(".... Eat...."); Out.Ln;
END Eat;
BEGIN {ACTIVE}
LOOP
Think;
fork[first].P; fork[second].P;
Eat;
fork[first].V; fork[second].V
END
END Philosopher;
VAR
philo: ARRAY NofPhilo OF Philosopher;
BEGIN
FOR i := 0 TO NofPhilo DO
NEW(fork[i], INTEGER(i));
NEW(philo[i], i);
END;
END Philo.
Philo.Philo1 ~
Ada (1980, последний действующий стандарт 2016)
Собственно, на первый взгляд тут есть все, что мне хотелось бы.
И даже чуть больше — есть числа с точным вычислениями с плавающей точкой. Например, есть риалтайм планировщик потоков, межпоточный обмен и формально верифицируемое подмножество языка SPARK. И еще много много всего.
Думаю, если бы для надежности Ады был нужен еще черт рогатый, он бы прилагался вместе с инструкцией по вызову в трудной ситуации =)
Реализация — ГНУтая Ада, развивается, стандартизована ISO/IEC.
Стандартом предусмотрена реализация с GC, но для компилируемых вариантов он чаще не реализован. Требуется ручное управление памятью — и тут возможны ошибки программиста. Впрочем, язык заточен на использование по умолчанию стека и есть понятие управляемых типов с деструкторами. Можно еще определить свою реализацию GC, автоосвобождения или подсчет ссылок для каждого типа данных.
Ada Reference Manual 2012 содержит 950 страниц.
Недостаток Ады кроме сложности — чрезмерная многословность, что впрочем было задумано в угоду читаемости. Из-за специфичности языковой модели безопасности, интеграция с “чужими” библиотеками затруднена.
На сайде Ada-ru есть хорошая обзорная переводная статья — первая ссылка.
-- Code from https://rosettacode.org/wiki/Dining_philosophers#Ordered_mutexes
-- ADA95 compatible so can run in ideone.com
with Ada.Numerics.Float_Random; use Ada.Numerics.Float_Random;
with Ada.Text_IO; use Ada.Text_IO;
procedure Test_Dining_Philosophers is
type Philosopher is (Aristotle, Kant, Spinoza, Marx, Russel);
protected type Fork is
entry Grab;
procedure Put_Down;
private
Seized : Boolean := False;
end Fork;
protected body Fork is
entry Grab when not Seized is
begin
Seized := True;
end Grab;
procedure Put_Down is
begin
Seized := False;
end Put_Down;
end Fork;
Life_Span : constant := 20; -- In his life a philosopher eats 20 times
task type Person (ID : Philosopher; First, Second : not null access Fork);
task body Person is
Dice : Generator;
begin
Reset (Dice);
for Life_Cycle in 1..Life_Span loop
Put_Line (Philosopher'Image (ID) & " is thinking");
delay Duration (Random (Dice) * 0.100);
Put_Line (Philosopher'Image (ID) & " is hungry");
First.Grab;
Second.Grab;
Put_Line (Philosopher'Image (ID) & " is eating");
delay Duration (Random (Dice) * 0.100);
Second.Put_Down;
First.Put_Down;
end loop;
Put_Line (Philosopher'Image (ID) & " is leaving");
end Person;
Forks : array (1..5) of aliased Fork; -- Forks for hungry philosophers
-- Start philosophers
Ph_1 : Person (Aristotle, Forks (1)'Access, Forks (2)'Access);
Ph_2 : Person (Kant, Forks (2)'Access, Forks (3)'Access);
Ph_3 : Person (Spinoza, Forks (3)'Access, Forks (4)'Access);
Ph_4 : Person (Marx, Forks (4)'Access, Forks (5)'Access);
Ph_5 : Person (Russel, Forks (1)'Access, Forks (5)'Access);
begin
null; -- Nothing to do in the main task, just sit and behold
end Test_Dining_Philosophers;
BetterC (dlang subset 2017, оригинальный D — 2001, D 2.0 — 2007)
Самая современная реализация из рассматриваемых. Полное описание языка довольно длинное — 649 страниц — см.оригинальный сайт.
Собственно это язык D, но с ограничениями ключом -betterC. Почему так ?!
Потому что стандартная библиотека D — Phobos, разрабатывается Александреску и получилась весьма хитромудрой, полностью построенной на шаблонах. Ключевое для данной темы, что Фобос неконтролируем в плане расхода памяти.
Самое важное что теряется в режиме BetterC — многопоточность, GC, строки, классы (структуры остаются — они близки по функционалу — только на стеке) и исключения (RAII и try-finally остаются).
Возможно, впрочем, часть программы писать на полном D, а критичную часть — на D -BetterC. Также есть системные атрибута функция для контроля неиспользования опасных эффектов: pure safe @nogc.
Обоснование режима от создателя языка.
А тут выжимка — что обрезано, а что осталось доступным.
Строки содержатся в Фобосе — и попытки их использовать в BetterC выливаются в адские ошибки инстантациации шаблонов на элементарных операциях вроде вывода строки на консоль или конкатенации. А в полном режиме D строки в куче и иммутабельные, потому операции с ними приводят к замусориванию памяти.
Мне приходилось несколько раз встречать жалобы на баги в компиляторе. Что впрочем неудивительно для языка, конкурирующего по сложности с С++. При подготовке статьи тоже пришлось столкнуться с 4мя ошибками — две возникли при попытке собрать dlangide новым компилятором и парой при портировании задачи о философах (например вылет при использовании beginthreadex).
Режим еще только недавно появился и ошибки, вызванные ограничением режима BetterC вылезают уже на этапе линковки. Узнать об этом заранее, какие фичи языка урезаны точно — приходится часто на собственном опыте.
// compile dmd -betterC
import core.sys.windows.windows;
import core.stdc.stdio;
import core.stdc.stdlib : rand;
//import std.typecons; // -impossible (
//import std.string; - impossible
extern (Windows) alias btex_fptr = void function(void*) /*nothrow*/;
//extern (C) uintptr_t _beginthreadex(void*, uint, btex_fptr, void*, uint, uint*) nothrow;
/* Dining Philosophers example for a habr.com
* by Siemargl, 2019
* BetterC variant. Compile >dmd -betterC Philo_BetterC.d
*/
extern (C) uintptr_t _beginthread(btex_fptr, uint stack_size, void *arglist) nothrow;
alias HANDLE uintptr_t;
alias HANDLE Fork;
const philocount = 5;
const cycles = 20;
HANDLE[philocount] forks;
struct Philosopher
{
const(char)* name;
Fork left, right;
HANDLE lifethread;
}
Philosopher[philocount] philos;
extern (Windows)
void PhilosopherLifeCycle(void* data) nothrow
{
Philosopher* philo = cast(Philosopher*)data;
for (int age = 0; age++ < cycles;)
{
printf("%s is thinking\n", philo.name);
Sleep(rand() % 100);
printf("%s is hungry\n", philo.name);
WaitForSingleObject(philo.left, INFINITE);
WaitForSingleObject(philo.right, INFINITE);
printf("%s is eating\n", philo.name);
Sleep(rand() % 100);
ReleaseMutex(philo.right);
ReleaseMutex(philo.left);
}
printf("%s is leaving\n", philo.name);
}
extern (C) int main()
{
version(Windows){} else { static assert(false, "OS not supported"); }
philos[0] = Philosopher ("Aristotlet".ptr, forks[0], forks[1], null);
philos[1] = Philosopher ("Kant".ptr, forks[1], forks[2], null);
philos[2] = Philosopher ("Spinoza".ptr, forks[2], forks[3], null);
philos[3] = Philosopher ("Marx".ptr, forks[3], forks[4], null);
philos[4] = Philosopher ("Russel".ptr, forks[0], forks[4], null);
foreach(ref f; forks)
{
f = CreateMutex(null, false, null);
assert(f);
}
foreach(ref ph; philos)
{
ph.lifethread = _beginthread(&PhilosopherLifeCycle, 0, &ph);
assert(ph.lifethread);
}
foreach(ref ph; philos)
WaitForSingleObject(ph.lifethread, INFINITE);
// Close thread and mutex handles
for( auto i = 0; i < philocount; i++ )
{
CloseHandle(philos[i].lifethread);
CloseHandle(forks[i]);
}
return 0;
}
Для сравнения, исходник на полном D.
На розетте также можно посмотреть варианты для прочих языков.
IEC 61131-3 ST (1993, последний стандарт 2013)
Нишевой язык программирования микроконтроллеров. Стандарт подразумевает 5 вариантов программирования, но писать прикладное приложение к примеру в релейной логике это еще то приключение. Потому сконцентрируемся на одном варианте — структурированный текст.
Текст стандарта ГОСТ Р МЭК 61131-3-2016 — 230 страниц.
Есть реализации для PC/x86 и ARM — и коммерческие, самая известная из которых — это CODESYS (часто еще и сублицензированная с разными именами) и открытые — Beremiz — с трансляцией через С.
Поскольку интеграция с С имеется, то подключить нужные для прикладного программирования библиотеки вполне реально. С другой стороны — в этой области принято, что логика крутится отдельно и только служит сервером данных для другой программы либо же системы — интерфейса с оператором или с СУБД, которая уже может быть написана уже на чем угодно — без требований реалтайма и даже каких либо временных вообще…
Многопоточное программирование для пользовательской программы появилось относительно недавно — в микроконтроллерах такое было раньше не нужно.
Приведение типов большей частью только явное (смягчено в последнем стандарте). Но контроль переполнения зависит от реализации.
В последней редакции стандарта появилось ООП. Обработка ошибок производится пользовательскими обработчиками прерываний.
Динамического выделения памяти для пользователя можно сказать что нет. Это исторически сложилось — количество данных, обрабатываемое микроконтроллером — всегда константно ограничено сверху.
(* Dining Philosophers example for a habr.com
* by Siemargl, 2019
* ISO61131 ST language variant. Must be specialized 4 ur PLC
* )
CONFIGURATION PLC_1
VAR_GLOBAL
Forks : USINT;
Philo_1: Philosopher; (* Instance block - static vars *)
Philo_2: Philosopher;
Philo_3: Philosopher;
Philo_4: Philosopher;
Philo_5: Philosopher;
END_VAR
RESOURCE Station_1 ON CPU_1
TASK Task_1 (INTERVAL := T#100MS, PRIORITY := 1);
TASK Task_2 (INTERVAL := T#100MS, PRIORITY := 1);
TASK Task_3 (INTERVAL := T#100MS, PRIORITY := 1);
TASK Task_4 (INTERVAL := T#100MS, PRIORITY := 1);
TASK Task_5 (INTERVAL := T#100MS, PRIORITY := 1);
PROGRAM Life_1 WITH Task_1:
Philo_1(Name := 'Kant', 0, 1, Forks);
PROGRAM Life2 WITH Task_2:
Philo_2(Name := 'Aristotel', 1, 2, Forks);
PROGRAM Life3 WITH Task_3:
Philo_3(Name := 'Spinoza', 2, 3, Forks);
PROGRAM Life4 WITH Task_4:
Philo_4(Name := 'Marx', 3, 4, Forks);
PROGRAM Life5 WITH Task_5:
Philo_5(Name := 'Russel', 4, 0, Forks);
END_RESOURCE
END_CONFIGURATION
FUNCTION_BLOCK Philosopher;
USING SysCpuHandling.library;
VAR_INPUT
Name: STRING;
Left: UINT;
Right: UINT;
END_VAR
VAR_IN_OUT
Forks: USINT;
END_VAR
VAR
Thinking: BOOL := TRUE; (* States *)
Hungry: BOOL;
Eating: BOOL;
HaveLeftFork: BOOL;
TmThink: TON;
TmEating: TON;
END_VAR
TmThink(In := Thinking; PT := T#3s);
TmEating(In := Eating; PT := T#5s);
IF Thinking THEN (* Just waiting Timer *)
Thinking := NOT TmThink.Q;
Hungry := TmThink.Q;
ELSIF Hungry (* Try Atomic Lock Forks *)
IF HaveLeftFork
IF SysCpuTestAndSetBit(Address := Forks, Len := 1, iBit := Right, bSet := 1) = ERR_OK THEN
Hungry := FALSE;
Eating := TRUE;
ELSE
RETURN;
END_IF
ELSIF
IF SysCpuTestAndSetBit(Address := Forks, Len := 1, iBit := Left, bSet := 1) = ERR_OK THEN
HaveLeftFork := TRUE;
ELSE
RETURN;
END_IF
END_IF
ELSIF Eating (* Waiting Timer, then lay forks *)
IF TmEating.Q THEN
Thinking := TRUE;
Eating := FALSE;
HaveLeftFork := FALSE;
SysCpuTestAndSetBit(Address := Forks, Len := 1, iBit := Right, bSet := 0);
SysCpuTestAndSetBit(Address := Forks, Len := 1, iBit := Left, bSet := 0);
END_IF
END_IF
END_FUNCTION_BLOCK
Safe-C (2011)
Экспериментальный С с удалением опасных фишек и с добавлением модульности и многопоточности. Сайт проекта
Описание примерно 103 страницы. Если выделить отличия от С — совсем мало, около 10.
Работа с массивами и указателями обезопасена, динамическая память с автоматическим подсчетом ссылок — с проверками на двойное освобождении и повисшие ссылки.
В стандартной библиотеке есть минимальный набор функций для GUI, многопоточности, сетевых функций (в т.ч http-сервер).
Но — данная реализация только для Windows x86. Хотя код компилятора и библиотеки открыт.
В рамках другой исследовательской задачи я собрал макет Веб-сервер, собирающий данные с IoT датчиков: 75 Кб исполнительный модуль, и < 1Мб частичный набор памяти.
/* Dining Philosophers example for a habr.com
* by Siemargl, 2019
* Safe-C variant. Compile >mk.exe philosafec.c
*/
from std use console, thread, random;
enum philos (ushort) { Aristotle, Kant, Spinoza, Marx, Russell, };
const int cycles = 10;
const ushort NUM = 5;
uint lived = NUM;
packed struct philosopher // 32-bit
{
philos name;
byte left, right;
}
philosopher philo_body[NUM];
SHARED_OBJECT forks[NUM];
void philosopher_life(philosopher philo)
{
int age;
for (age = 0; age++ < cycles; )
{
printf("%s is thinking\n", philo.name'string);
delay((uint)rnd(1, 100));
printf("%s is hungry\n", philo.name'string);
enter_shared_object(ref forks[philo.left]);
enter_shared_object(ref forks[philo.right]);
printf("%s is eating\n", philo.name'string);
delay((uint)rnd(1, 100));
leave_shared_object(ref forks[philo.right]);
leave_shared_object(ref forks[philo.left]);
}
printf("%s is leaving\n", philo.name'string);
InterlockedExchange(ref lived, lived-1);
}
void main()
{
philos i;
assert philosopher'size == 4;
philo_body[0] = {Aristotle, 0, 1};
philo_body[1] = {Kant, 1, 2};
philo_body[2] = {Spinoza, 2, 3};
philo_body[3] = {Marx, 3, 4};
philo_body[4] = {Russell, 0, 4};
for (i = philos'first; i <= philos'last; i++)
{
assert run philosopher_life(philo_body[(uint)i]) == 0;
}
while (lived > 0) sleep 0; // until all dies
for (i = philos'first; i <= philos'last; i++)
{
destroy_shared_object(ref forks[(uint)i]);
}
}
Напоследок — сводная таблица соответствия функциональным требованиям.
Наверняка я что то упустил или переврал — так что поправляйте.
Исходники из статьи на гитхабе.
Комментарии (95)
red75prim
03.03.2019 09:47А что демонстрируется? Что даже в безопасных языках можно достичь взаимной блокировки?
Используемый алгоритм входит в блокировку, если выпавшие псевдослучайные числа и работа планировщика потоков приводят к тому, что сначала выполняются все инструкции «взять левую вилку».Tsvetik
03.03.2019 10:12Интересный язык ADA. Сложный, но со множеством возможностей.
К сожалению, большинство «вкусняшек» зависят от ADA-runtime. А для микроконтроллеров есть только профиль Ravenscar, который поддерживает не все возможности языка.TargetSan
03.03.2019 19:50+1Я честно говоря так и не понял, о какой безопасности говорят сторонники Ada. В языке с исключениями, при отключенной сборке мусора, предполагается ручное на уровне С управление ресурсами. А RAII сделан через отдельный базовый класс, что сильно срезает его полезность. Т.е. возможностей отстрелить себе аллоцированный ресурс по самый thread header больше, чем в C++.
Tsvetik
03.03.2019 20:31Я Аду не знаю, но интересовался в приложении к программированию МК.
В подмножестве SPARK есть формальная верификация. Т.е. компилятор доказывает, что при любых входах программа будет работать корректно.
Синтаксис спроектирован так, чтобы при написании кода программист допускал меньше ошибок. Поэтому синтаксис сильно многословен.
Есть множество проверок, которые проводятся как на этапе компиляции так и в рантайме. Например, всякие переполнения, контроль точности операций с плавающей точкой, есть встроенная математика с фиксированной точкой.
Есть руководство по стилистике кода.
Функциям можно давать разные ограничения на аргументы и возвращаемые значения. Компилятор их будет проверять.
Работа с многозадачностью устроена на уровне языка. Задачи общаются друг с другом с помощью сообщений.0xd34df00d
04.03.2019 18:52компилятор доказывает, что при любых входах программа будет работать корректно
Как определяется корректность? Как отсутствие, условно, undefined behaviour или как соответствие спеке? Если второе, то как описывается спека?
Tsvetik
04.03.2019 20:32Я не специалист по Аде.
Если я правильно понимаю, то в SPARK описываются те или иные условия, которые должны выполняться в процессе работы программы. Думаю, их можно понимать как assert в Си. А далее некоторый инструмент gnatProve проходит по программе и убеждается, что все условия выполняются при любых входах. Причем, на этапе компиляции, а не в рантайме.0xd34df00d
04.03.2019 21:51Насколько выразителен язык описания условий? Что именно в виде этих условий можно выразить?
Понятно, что выразительность уровня assert несовместима со статической верификацией, ибо там рядом где-то проблема останова.
OCTAGRAM
03.03.2019 20:49Те, кто приходят с других языков и по привычке смотрят, что там с указателями, смотрят не туда. Предполагается, что в ультраидиоматичных адских программах голые указатели вообще не проскакивают. А ресурсами управляют, например, контейнеры. Лежит в карте где-то запись, навёл на неё Cursor, написал declare-begin-end, между declare и begin прорубил через renames окно (Ada 2012 reference) в эту запись, и работаешь с ней. При включенных защитах от tampering это окно ещё по принципу RAII удерживает блокировку на контейнере. Как из end вышел, всё, нет окна, нет блокировки, кроме, разве что, от Cursor.
TargetSan
03.03.2019 21:03Окей. Ткните меня пожалуйста носом в аналог
std::unique_ptr
,std::shared_ptr
,std::weak_ptr
. Я серьёзно. Потратил часа два или три и так и не нашёл. Т.е. что делать если мне нужно в контейнер положить не само значение, а ссылку на него?OCTAGRAM
03.03.2019 21:34Из ParaSail собираются заимствовать уникальные указатели. Они семантически похожи на записи с дискриминантом, на них наконец-то удалось натравить хоть какую-то верификацию, а если что-то новое можно верифицировать, оно идёт в язык Ада и SPARK. Будучи экономическим фундаментом, SPARK — это обстоятельство непреодолимой силы. Разделяемые ссылки в этом смысле плохие, и в ISO стандарт не идут, а так в библиотеках пруд пруди.
www.dmitry-kazakov.de/ada/components.htm#Objects_etc
www.adacore.com/gems/gem-100-reference-counting-in-ada-part-3-weak-references
Ещё реализацию видел у Вадима Годунко в Матрёшке, а сам я пользуюсь собственной, которая работает как мне надо.TargetSan
03.03.2019 21:42Т.е. вы хотите сказать, что в языке с упором на безопасность и корректность до сих пор нет инструментов из коробки для управления ресурсами без сборки мусора?
OCTAGRAM
03.03.2019 21:53И какое такое нужно управление ресурсами?
В том, что я видел с упором на безопасность и корректность, нет указателей. Либо глобально размещено, либо на стеке какой-то задачи. Вот в Ironsides, SPARK-верифицированном DNS-сервере нет указателей, потому что та версия SPARK, под которую он писался, их не поддерживает. Это не мешает ему использовать контейнеры. Просто это контейнеры такие специальные, которые параметризуются максимальной вместимостью и занимают сразу максимум места, а вместо указателей там индексы.
С точки зрения системного администратора управление ресурсами — это не когда программа решила, сколько ей ресурсов, а когда системный администратор решил, сколько программе ресурсов, и так оно и есть. Вот SPARK, безопасность, корректность — это в первую очередь для таких людей.
А если на один участок памяти может быть более одного указателя, статически не отождествимых с одним, то всё, тут уже понятно, что это какая-то другая область с расслабленными требованиями начинается.TargetSan
03.03.2019 21:56Корректно удалить объект при выходе из скоупа? Например, закрыть файл? Несмотря ни на какие исключения.
TargetSan
04.03.2019 11:32Мне кажется, проблема в том, что мы не совсем об одном и том же разговариваем. Вы, похоже, говорите в основном про SPARK, который хоть и статически верифицируем, но в силу специфики имеет ограниченный круг применения. Я в основном говорю про Ada в общем. Так о чём будем продолжать разговор? Если про SPARK — предлагаю закончить, т.к. там благодаря стат. верификации большинства рантайм проверок и так не будет. И проблем с "не закрыли файл" тоже. Просто не во всех приложениях можно на этапе проектирования просчитать, сколько оно сожрёт ресурсов. Я бы сказал, в очень небольшом числе приложений.
OCTAGRAM
03.03.2019 21:50Список runtime проверок, определённых стандартом языка Ада
Список дополнительных runtime проверок, определённых GNAT
Из не совсем runtime: protected может работать как рвлок. При этом на чтение со множественным доступом содержимое-таки действительно видно в режиме только чтение. Также может работать как монитор Хоара. При этом условные переменные сигналятся автоматом. Куча таких мелочей делают жизнь проще.
red75prim
03.03.2019 10:38Пример на Rust с демонстрацией блокировки.
Кодextern crate crossbeam; // 0.7.1 use std::sync::Mutex; use std::thread::sleep; use std::time::Duration; fn philosopher(id: &str, left_fork: &Mutex<()>, right_fork: &Mutex<()>) { for _ in 0..5 { println!("{} ждёт левую вилку", id); let left_fork = left_fork.lock().unwrap(); println!("{} взял левую вилку", id); // Если раскомментировать следующие строки будет deadlock //println!("{} думает...", id); //sleep(Duration::from_millis(100)); println!("{} ждёт правую вилку", id); let right_fork = right_fork.lock().unwrap(); println!("{} взял правую вилку", id); println!("{} ест...", id); sleep(Duration::from_millis(100)); drop(right_fork); println!("{} положил правую вилку", id); drop(left_fork); println!("{} положил левую вилку", id); println!("{} думает...", id); sleep(Duration::from_millis(100)); } } fn main() { let philosophers = vec![ "Аристотель", "Сенека", "Платон", "Сократ", "Анаксогор", ]; let n = philosophers.len(); let mut forks = vec![]; for _ in 0..n { forks.push(Mutex::new(())); } crossbeam::scope(|s| { for i in 0..n { let id = &philosophers[i]; let left_fork = &forks[i]; let right_fork = &forks[(i + 1) % n]; s.spawn(move |_| philosopher(id, left_fork, right_fork)); } }) .unwrap(); }
third112
03.03.2019 11:46+1Не понял итоговую таблицу «Надежность языков программирования». Среди ЯП «Pascal» и «Паскаль» это 2 разных языка?;) При этом для первого во 2ой колонке ничего не указано, для втоторого «громозкий исходник», «плохой оптимизатор», «огромный.екзешник» (пунктуация авторская, видимо по аналогии с расширением файла ".exe" перед словом «екзешник» поставлена точка ;) А где упомянутый «громозкий исходник»? — в статье его нет.
Про «Паскаль» только 1 фраза:
Active Oberon (2004)
Создавался с оглядкой на опыт Паскаля, Модулы, предыдущих Оберонов с 1988г, Java, C#, Ады, а также практический опыт применения.
(а про «Pascal» ничего). Далее в следующих столбцах таблицы «Pascal» vs «Паскаль»:
«выделить главное» vs «бардак с разыми типами строк», «разделить int и float» vs «ничего особого», в столбце «Контроль границ массивов, коллекций итп» для «Pascal» ничего, а у «Паскаль» это «есть» и т.д. И наконец у «Паскаль» "«есть генерики, ООП», а у «Pascal» нет? Но известно, что в стандартном (ISO 7185:1983, ANSI/IEEE 770X3.97:1983) Pascal (и Паскале) ООП нет, а есть ОО-Паскаль (ANSI/X3-TR-13:1994) и не один. BTW самой нижней строкой в таблице идет Delphi, но про этот продукт ничего нет. И опять ИМХО странное выделение Delphi в отдельную строку — IDE Delphi с точки зрения ЯП — это ОО-Паскаль, как, нпр., был Think Pascal для классических Маков. Возвращаясь к процитированной фразе из статьи возникает вопрос: чем опыт Паскаля (и др.) был хуже опыта Active Oberon? В контексте статьи хорошо бы начать с доказательства, что ООП повышает, а не понижает надежность. Может стандартный (не ОО) Паскаль надежнее, чем ОО-Паскаль и чем Оберон?
И снова о таблице: приведенные коды обедающих философов никак в ней не упомянуты — нет никаких выводов из них. Зачем тогда столько кода? Что он доказывает? Ну, иллюстрация синтаксических особенностей ЯП, но это в Википкдии есть для почти каждого ЯП (даже для некоторых эзотерических). В статье кратко сказано:
Недостаток Ады кроме сложности — чрезмерная многословность
Из столь короткого листинга я не заметил ни сложности, ни многословности. Т.е. нет анализа приведенного кода философов, каковой анализ позволил бы сделать такие выводы.saipr
03.03.2019 13:14+1Как давно это было:
От Паскаля к Аде/ Т.Ю.Бардинова, В.Ю.Блажнов, А.А.Маслов, В.Н.Орлов. — 1990
Москва, Финансы и статистика, 1990. 255 с. Твердый переплет.
Аннотация: В книге рассматриваются основные приемы программирования на языках Паскаль и Ада. Изложение материала сопровождается большим количеством примеров программ, иллюстрирующих аналогичные возможности обоих языков программирования.
Одна из первых книг по языку программирования ADA/АДА.
third112
03.03.2019 13:21Хорошая книга. В контексте статьи ИМХО стоит упомянуть еще:
Языки программирования Ада, Си, Паскаль. Сравнение и оценка
ред. Фьюэр, А.; Джехани, Н.
Издательство: М.: Радио и связь; 1989 г.
OCTAGRAM
03.03.2019 13:28Как давно это было
Как насчёт освежить?saipr
03.03.2019 13:30А это как?
third112
03.03.2019 13:44Нпр., сделать новый язык, совместимый со старыми на уровне исх. кода. В 1ой части обсуждаемой статьи автор справедливо отметил:
Устойчивость к ошибкам человека
Среди этих ошибок стоит указать и перенос кода со старого ЯП на новый. В некоторых парах языков «старый-новый» перевод проходит сравнительно легко, а в некоторых тяжело и ведет к трудноуловимым багам. Особенно в нередких случаях, когда переводчик-кодер пытается ускорить работу и не вдумывается в алгоритм, реализованный в переносимом коде.
third112
03.03.2019 13:35Похоже, к тому идет. Казалось повесили ярлык «устаревшие ЯП» и совсем забыли, но всё чаще и чаще вспоминают.
Siemargl Автор
03.03.2019 15:18Эмм, это как в той диссертации — «все равно до сюда никто не дочитает» =)
В один прекрасный момент возникла мысль — «А почему бы не Паскаль?» — и это черновые наброски — не имеющие во многом отношения к надежности (размер или оптимизатор).
В итоге я забыл поправить финальную таблицу. Исправим.
Паскаль — получился не лучше остальных в своей группе (и так там много участников) и главное — непонятно, то ли ISO Паскаль рассматривать, то ли Delphi диалект? — но Оберону проигрывают в надежности оба. Потому не попал в итоговый вариант статьи.
Спс за внимательность.
Из столь короткого листинга я не заметил ни сложности, ни многословности. Т.е. нет анализа приведенного кода философов, каковой анализ позволил бы сделать такие выводы.
На этом примере это не очень очевидно — но стоит посмотреть другие исходники и текст стандарта. И так статья раздута — и не претендует на качественный анализ.third112
03.03.2019 15:37это как в той диссертации — «все равно до сюда никто не дочитает» =)
Опытные оппоненты диссеры с конца читают ;)
Паскаль — получился не лучше остальных в своей группе (и так там много участников)
Какие параметы для принадлежности к этой группе? И кто еще? — хотя бы несколько примеров. И почему Паскаль не лучше?
непонятно, то ли ISO Паскаль рассматривать, то ли Delphi диалект?
Действительно. И с Delphi непонятно. До Delphi-7 было просто: Delphi-N+1 лучше Delphi-N, а потом нарушилась совместимость. Для GUI Delphi удобнее, нпр., турбо-Паскаля, но не очевидно, что надежнее.
но Оберону проигрывают в надежности оба.
Почему? ИМХО неочевидно.Siemargl Автор
03.03.2019 16:03Группа — это Паскаль, Оберон, Модула.
Проигрывает АО из-за ручного управления памятью и многопоточностью. Также нетипизированные указатели и приведение типов никуда не делись.
Но поскольку это языки одной группы — разница небольшая.third112
03.03.2019 17:07Проигрывает АО из-за ручного управления памятью и многопоточностью.
Тут про какой Паскаль речь, нпр., в Дельфи:
Тип string — автоматический распределяемый в памяти, с подсчётом ссылок и парадигмой Copy-On-Write. В поздних версиях Delphi символы двухбайтные, Unicode-совместимые.
Но в общем автоматическая сборка мусора в плане надежности оценивается неоднозначно.
Управления многопоточностью уже в Дельфи-7 было достаточно удобным. И с OpenMP особых проблем не было.
Но поскольку это языки одной группы — разница небольшая.
При небольшой (допустим) теоретической разнице, очень большая практическая разница. Оберон и Модула использовались заметно меньше, чем Паскаль. Меньше накоплено опыта, меньше специалистов, меньше кода, меньше публикаций. Всё это на практике не способствует надежности.
OCTAGRAM
03.03.2019 16:33Вообще говоря, у Delphi был неплохой задел. Но Delphi — это два языка в одном. Есть один язык, в котором и есть те самые неплохие заделы, и есть язык, который поддерживается.
В первом языке проверка целочисленных переполнений и диапазонов. В первом языке открытые массивы (в терминах ISO Pascal согласованные массивы, conformant arrays). В первом языке отличные от чисел перечисления. В первом языке ARC существует пусть хотя бы на COM интерфейсах.
Но первый язык не развивают, а развивают второй язык, где объекты с ручным управлением памятью, свойства, события и прочая излишне распиаренная хелсберговщина.
Второй язык развивается и продвигается, а первый язык прозябает в стагнации и безвестности. Вот, например, как были со времён Турбо Паскаля проверки целочисленного переполнения и диапазонов, так и остались почти без изменений. Ну разве что Assert добавились. А что, больше проверять нечего стало? nil можно было бы не ломиться разыменовывать, чтоб упереться в EAccessViolation, а проверить. А ещё, как в Ada 2005, можно дать синтаксис, чтоб запретить nil. В Ada 2005 not null может стоять везде, хоть в record. Это возможно сделать, потому что в языке Ada есть три фичи, которые делают возможным и удобным обращаться с такими структурами данных.
- Во-первых, при объявлении record можно сразу же и задать значение по умолчанию. Скорее всего, так не будет сделано, но возможность есть.
- Во-вторых, есть агрегаты, которые можно использовать везде, не только при инициализации глобальных переменных. И если значение по умолчанию не задано, а null невозможно принять по умолчанию, потому что он запрещён not null, разработчик может использовать агрегат.
- В-третьих, можно инициализировать любую переменную, не только лишь глобальную. В языке Ада это с первых версий, с 1983го года, в Delphi это появилось только в этом 2019м году, в версии 10.3 (Rio).
За счёт этого компилятору Ады есть, к чему принудить разработчика. Если же в Delphi всего этого не было, то пропустив азы, сразу в мир надёжности не вскочишь, но хотя бы в аргументах функций можно было бы nil запрещать. Могли. Но не сделали.
Идём далее. В ISO Pascal есть такая возможность, как conformant array parameters. В языке Ada она специального имени не имеет, но unconstrained arrays, если их принимать формальным аргументом, так себя ведут. Существует изначально, с 1983го года. В языке Delphi это называется open arrays. Существует с 90х, версия Delphi 4 или около того. В C++ что-то похожее появилось только в C++20, std::span. Можно такие параметры из обычных массивов делать, можно из динамических. Можно передать по цепочке принятый формальный аргумент такого типа. А ещё можно сузить, можно передать поддиапазон значения. Дебилизм в Delphi состоит в том, что псевдофункция Slice, единственный способ скрафтить суженное значение, может обрезать справа, но не слева, в отличие от Copy, создающей новое значение. Какого-то обоснования такому положению вещей я не вижу. Манипулируя с указателями, я могу добиться того, чтобы в функцию-таки передать обрезанный с другой стороны подмассив, но тогда компилятор не вполне способен проверить, не было ли выхода за границы диапазона. Это выглядит, будто тёмный угол, в который давно никто не заглядывал.
Ещё по мелочи хотелось бы, чтоб Boolean(5) не работал, а бросал исключение.
У меня есть опыт, как я устраивался на работу, включал в проекте проверки ошибок, и каааак повсплывало. Даже то немногое, что есть в Delphi, показало себя очень полезным.
С Адой им не тягаться, но у производителя по разным фичам была фора лет в пятнадцать прежде, чем они дойдут даже до жирафов C++. Всё это время могли бы выезжать на этой волне. И даже когда доходят, могли бы на конференциях выступить, типа
А вот вы знаете, когда вашего Rust ещё даже в проекте не было, у тех, кто программировал на Delphi, уже были и проверки диапазонов, и отлов целочисленных переполнений, и даже с барского стола перепали open arrays. Мы, правда, будучи кусками дебилов, забыли включить их по умолчанию, и чтоб уж дебилизм был последовательным, прорекламировать включить тоже забыли, но теперь-то мы исправимся. И по умолчанию включим, и Slice починим, и всё это последовательно будет, а не спонтанными подачками.
Сложный, противоречивый язык программирования получается. Отличные заделы плюс безбожный слив со стороны производителя.
phantom-code
03.03.2019 11:49Язык D очень интересный и по ощущениям, весьма продуктивный. Но у него есть несколько моментов, ставящих в тупик. Например, транзитивный const. При всей кажущейся разумности идеи, это выливается практически в невозможность использования const. Один из частых советов на форумах D: «don't use const». Кроме того, отсутствие конструктора по умолчанию для struct и конструктора копирования (правда сейчас обсуждается предложение по его добавлению) так же порой доставляет много неудобств.
Siemargl Автор
03.03.2019 15:25С const и в С++ проблема — просто надо привыкнуть к проектированию архитектуры. Один из вариантов — элементарно 2 варианта ф-ции с const и без.
Про конструкторы создания и копирования структур добавили жеphantom-code
03.03.2019 15:29Конструкторы копирования еще обсуждаются (идет финальный раунд), вы путаете с postblit конструкторами (вызывается после memcpy данных).
А конструктора по-умолчанию у структур нет, т.к. в D все типы должны иметь «значение по-умолчанию» (.init).Siemargl Автор
03.03.2019 15:47Я не путаю, я считаю что postblit достаточно. Аналогично с инициализацией структур по умолчанию.
Остальное в этом DIP — абстрактные игры разума, не нужные на практике (ок, наверняка возможно придумать пример нужности).
Такие вещи и угробили D2 — ненужное переусложнение. К огромному моему сожалению — я даже TDPL с Амазона купил (
OCTAGRAM
03.03.2019 14:13
Языки программирования. Концепции и принципы
Кауфман В.Ш.
О книгеРассмотрены фундаментальные концепции и принципы, воплощенные в современных и перспективных языках программирования. Представлены разные стили программирования (операционный, ситуационный, функциональный, реляционный, параллельный, объектно ориентированный). Базовые концепции и принципы рассмотрены с пяти различных позиций (технологической, авторской, математической, семиотической и реализаторской) и проиллюстрированы примерами из таких языков, как Паскаль, Симула-67, Смолток, Рефал, Ада, Модула-2, Оберон, Оккам-2, Турбо Паскаль, С++ и др. Сложность выделена как основополагающая проблема программирования, а абстракция-конкретизация и прогнозирование-контроль – как основные ортогональные методы борьбы со сложностью. На этой общей базе в книге впервые представлена цельная система концепций и принципов, создающая чёткие ориентиры в области языков программирования. На основе этой системы сформулированы оригинальные положения, указывающие перспективы развития в этой области (модули исключительных ситуаций, модули управления представлением, входовые типы и др.). Многие из них в последние годы стали реальностью. Новые подходы применены при изложении известных фактов (пошаговая модификация нормальных алгоритмов Маркова сначала до Рефала, а затем до реляционных языков, сопоставление принципов «сундука» и «чемоданчика» при создании Ады, Модулы-2 и Оберона, развитие концепции наследуемости от модульности до объектной ориентации, систематическое сопоставление концепции параллелизма в Аде и Оккаме-2, и др.). Для всех, серьёзно интересующихся программированием, в том числе научных работников, программистов, преподавателей и студентов.third112
03.03.2019 15:50+1У этого автора была интересная журнальная статья, что каждый ЯП имеет свои подводные камни (свои неоднозначности). Эти камни и являются основным источником проблем. С выявления этих камней и надо в первую очередь начинать оценку ЯП.
saipr
03.03.2019 14:13+1На мой взгляд надежное программирование это все же впервую очередь стиль, манера, искусство программирования. Я зык здесь помощник. Надежная программа всегда должна корректно завершаться. Именно корректно завершаться. Она может не найти решение в какой-то ситуации, но честно об этом сообщить пользователю. И тот в этом случае поймет ее (программу), ну и будет принимать решение.
Siemargl Автор
03.03.2019 15:28Не согласен. Например ПО управления автомобилем — извините, завершилось =)
Автоматический перезапуск и циклический анализ ситуаций — типичный кстати для IEC 61131-3, здесь гораздо лучше.OCTAGRAM
03.03.2019 19:07Да и в игре пусть лучше поведение NPC попадёт в сюжет Мармока, чем аварийно завершит всю игру.
third112
03.03.2019 15:56Я зык здесь помощник
Но помощники разные бывают. Нпр., ассемблер вряд ли кто сегодня выберет, если можно использовать ЯП высокого уровня. И QBasic не многие сегодня выберут ;)
struvv
03.03.2019 16:57+1По идее должны быть рассмотрены языки типа Idris, т.к. только в семействе таких языков есть реальные compile time проверки, позволяющие полностью исключить любые ошибки, кроме ошибок бизнес логики(по очевидным причинам), включая невозможность падения программы от деления на ноль
0xd34df00d
03.03.2019 18:31Да, оставлять Idris, Agda и прочие Coq без внимания несколько странно.
Sirikid
03.03.2019 19:32Agda и Coq не вычисляются, а согласен ли автор на экстракцию — вопрос. Тем более на экстракцию в Haskell.
OCTAGRAM
03.03.2019 19:03SPARK был упомянут, но можно что-то ещё, да
struvv
04.03.2019 13:47разве SPARK имеет отношение к автоматическому доказательству теорем?
Sirikid
04.03.2019 20:32Idris, Coq и Agda тоже не имеют.
0xd34df00d
04.03.2019 21:52А чего, obvious proof search в идрисе или crush tactic в коке (и его гипотетический аналог в виде elab script в идрисе) не про это? :]
Sirikid
04.03.2019 23:50Coq и Agda это все же proof assistants, то есть они только проверяют человеческие доказательства, тактики в Coq доказывают либо простые теоремы, либо в специфических разрешимых случаях. А Idris это вообще ЯП общего назначения, хоть и с зависимыми типами и с некоторым выводом термов.
Ссылки по теме: Proof assistant, Automated theorem proving. В последней, кстати, упомянается и SPARK. На мой вкус условия там достаточно разнообразны и напоминают таковые у Liquid Haskell, но со спецификой Ады.0xd34df00d
05.03.2019 01:08Да это я так, в штуку про идрис и не очень в шутку про coq.
У coq'а ещё, я слышал, есть интеграция с SMT-солверами и возможность получать доказательство (или контрпример) от них для значимого ряда практически интересных случаев. Но конкретно этой ветвью я не очень интересовался.
OCTAGRAM
03.03.2019 19:51В связи с Better-C можно ещё упомянуть CCured и Deputy. CCured — это такой транслятор Си->Си, который делает указатели жирными, но по возможности как можно менее жирными. Специальный анализатор отслеживает все потоки данных и выбирает степень жирности каждого указателя, которой было бы достаточно для того, чтобы все требуемые операции над ним были безопасно реализуемы. Самый плохой указатель WILD, и он как чума всё заражает. Внутри структур, на которые ссылается WILD, могут быть только WILD указатели.
Работа по отмыванию устаревшего кода от грязи начинается с того, что переписыванием фрагментов разработчик пытается устранить WILD совсем. Авторам удалось отмыть от грязи достаточно большие массивы устаревшего кода, и пока они это делали, они обогатили свой транслятор различной полезной семантикой. Чтоб, например, можно было в своём коде делать проверки, а в код, который ну никак нельзя поменять, передавать структуры без жирных указателей, есть расщепление структур.
Из всех проектов по отмыванию унаследованного кода от грязи это самый продвинутый. На пути отмывания от грязи следующим этапом после принуждения к инкапсуляции памяти, казалось бы, должен быть порт на Аду, но нет, Ada is not invented here. В качестве самодостаточного языка программирования, не для старого кода, а для нового, у них самоделка Deputy по тем же лекалам, что и CCured. Для полноты можно упомянуть.
С C++ подобную штуку, похоже, невозможно нормально скрестить, так как и шаблоны, и анализатор минимальной жирности входят в конфликт. Единственно работающие способы отмыть C++ от грязи я вижу в CHERI и Эльбрус2000, то есть, максимально жирные указатели для всего. В то время, как в CCured большую часть указателей автоматом удаётся облегчить, а дальше разработчик устраняет оставшиеся WILD, в C++ эта работа даже не может начаться. Писать на C++ это такое попадалово, что потом вовек не отмыться. К сожалению, никто (Cyclone и др. отмывальщики C) не пошёл другим путём, в сторону Objective-C. Там, похоже, таких проблем, как с C++, нет, и можно было бы наполнить экосистему безопасным кроссплатфоренным GUI и программами на нём.
Для надёжных языков программирования поднятый вопрос актуален, потому что каждый bzip2 с нуля быстро не перепишешь, а если подключишь неотмытый libbzip2, то через него-то тебя и ломанут. Надо исследовать возможности, как отмыть унаследованные библиотеки на Си перед тем, как подключать их в свой код на надёжном языке.
BD9
04.03.2019 00:56Стоит упомянуть про Автоматическое доказательство.
Контрактное программирование (программирование с обязательствами) упоминается один раз на статью, а оно должно быть основой.
Даже не упоминается язык Eiffel, который с успехом заменит Паскаль, Дельфи, Оберон, Модулу и прочие паскалеподобные (алголоподобные), кроме Ады со СПАРКом. У Эйфеля есть хорошая бесплатная (для GPL) среда разработки.
Эйфель — замечательный язык, но спрос на него близок к нулю (В СНГ — равен нулю).
А в общем — чем совершеннее язык, тем он сложнее (для понимания средним программистом), чем сложнее — тем меньше используется, мало используется — его забывают.
Ada хотя бы нашла свою нишу.
inv2004
Я извиняюсь если пропустил, но чём именно обусловлен выбор именно этих языков? Я в том плане, что когда речь про надёжность — то это основная тема для Rust, а его тут нет.
staticlab
Читайте предыдущую статью.
AngReload
Там написано «есть и другие, но рассматривать я их не буду», что как бы не ответ на вопрос.
Но вообще, лично я вижу сильное различие между Rust и любым языком из этого списка — я бы низачто не стал бы писать на них.
OCTAGRAM
Значит, программировать беспилотные автомобили в NVIDIA не судьба
Siemargl Автор
ОК, по таблице есть желание дополнить по пунктам?
Навскидку я вижу не более 50% соответствия, но я не знаю Раст.
AngReload
Вы не подумайте что я ратую за Rust. Просто после прочтения статьи сложилось такое впечатление, что это языки которыми уже никто не занимается, без сообщества, с вылезающими на простой простейшей программе древними багами, без инструментов, без менеджера пакетов, и где-то даже без компилятора. Я лишь чуть изучаю Rust, он тоже заявлен как безопасный язык, и совсем не похоже чтобы там были такие проблемы.
JekaMas
Думаю, они, скорее специфичны и задачи у них специфичные. Пример с автомобилем отличный. Оберон вроде приживался еще в энергетике.
OCTAGRAM
Языки есть с одним владельцем. Он там поливает территорию вокруг себя, делает благообразно. Но чужие там не ходят. А есть демократичные. Там больше одного производителя, но и анархия. Везде свои сильные и слабые стороны.
TargetSan
Попробую, хотя у Вас в некоторых пунктах намешано много всего
В целом Rust удовлетворяет бОльшей части Ваших требований из коробки либо позволяет их реализовать сравнительно легко. К сожалению, требования недостаточно чётко поставлены, чтобы можно было однозначно ответить на них.
OCTAGRAM
Тут ещё надо уточнить, что такое паники. Вот взять Delphi, Ada, Rust. Казалось бы, везде проверка целочисленных переполнений и диапазонов есть.
Но если вдаться в детали, в Delphi и Ada оно приводит к легко уловимому exception, а в Rust случается паника. А паника в Rust не то же что исключение. Для отлова паники можно использовать функцию, принимающую два замыкания, первое — что нужно сделать, второе — что сделать, если поймали панику. Кажется, это похоже на обработчик исключений, но нет, опять не угадали. Перед тем, как упасть вниз по стеку, до точки, где установлен перехват паник, ещё успевает нагадить в консоль обработчик паник. Насколько я понимаю, этот обработчик тоже можно отключить или заменить более молчаливой версией. В программе такое можно сделать, а в библиотеке? Нормально ли будет, если какая-то библиотека заменит глобальный обработчик паник? Или если будет полагаться на то, что он отключён, и преспокойно себе бросать и ловить паники.
Всё это похоже на Turbo Pascal образца конца 80х. Там тоже целочисленные переполнения и выход за границы диапазона были. НО ВАЖНО КАК ОНИ БЫЛИ. Там же не было структурной обработки исключений. Там было прерывание, прерывание можно было гипотетически перехватить. Структурной обработки исключений нет, поэтому что делать обработчику прерываний, интересный вопрос. Лучшее, что можно было придумать, это на SetJmp/LongJmp сделать что-то вроде SEH с RAII. Как и в случае Rust, не приходится ожидать, что это сделано в библиотеках.
Так что по факту этот механизм не работает, или работает отнюдь не в полную силу, не так, как в других языках программирования.
Sirikid
Паники это не исключения и они не должны использоваться вместо исключений. Хотите обрабатывать ошибки — используйте Option или Result.
OCTAGRAM
Где взять плюс, минус, умножение для чисел, чтоб возвращали Option или Result? Я что-то не нашёл.
TargetSan
https://doc.rust-lang.org/std/primitive.i32.html#method.checked_add и далее вниз по доке. Для остальных примитивов аналогичный набор.
OCTAGRAM
А, понятно. Исписываем всё в checked_add, checked_sub и checked_mul и думаем, чёрт возьми, вот она, эргономика. Правда, при этом чужие, не столь эргономично написанные библиотеки предательски норовят выдать панику.
TargetSan
К сожалению, любое решение имеет свою цену. К примеру, исключения позоляют рапортовать любую ошибку откуда угодно. Но приводят к тому, что необходимо реально ждать такой ошибки из каждой щели. Почитайте про weak/strong exception guarantee в С++. В некоторых случаях обеспечение даже слабой гарантии превращает код в лапшу.
OCTAGRAM
В поисках лучших практик чтиво по C++ будет болтаться где-то в конце списка.
TargetSan
А вы почитайте. Про то, как надо побиться головой об стену чтобы обеспечить инварианты в условиях могущих вылететь откуда угодно исключений.
TargetSan
Давайте немножко разделим.
По поводу обработки числовых переполнений. Здесь КМК столкнулись требования zero overhead и безопасности. Во-первых, в Rust сознательно отказались от исключений в пользу Result. Следовательно, бросить исключение из оператора сложения мы не можем. Иначе был бы C++ "anything can throw". К тому же, проверка каждой операции приводила бы к оверхеду. Результатом был бы жуткий срач. Далее, делать всю арифметику return Result — убить эргономику. Ещё один потенциальный срач. Для тех, кому нужна предсказуемая арифметика, у каждого целочисленного типа Rust есть набор методов checked/saturating/wrapping/overflowing. У чисел с плавающей точкой есть свой набор контроллируемых операций.
Теперь, по поводу паник. Паники предназначены для выражения ошибок "Шеф! Всё пропало!". По умолчанию паники реализованы через С++-подобный механизм исключений, но можно реализовать свой паник хендлер либо выставить panic=abort. По умолчанию поймать панику можно — std::panic::catch_unwind.
OCTAGRAM
catch_unwind — это тот самый, который срабатывает уже после того, как консоль загажена
TargetSan
https://doc.rust-lang.org/std/panic/fn.set_hook.html
OCTAGRAM
Глобальные обработчики прерываний, цепочки обработчиков прерываний, DOS, 15дюймовый электроннолучевой дисплей формата 4:3, Turbo Pascal, EGA. Сколько воспоминаний.
Это, я так понимаю, тот самый глобальный обработчик, которым не комильфо рулить из библиотек, но и оставлять как есть не хочется.
Sirikid
Это глобальный обработчик глобального же пиздеца — все сходится.
OCTAGRAM
Из тех альтернатив, которые я видел, кажется, что именно в языке Ада сделан удобный выбор. Либо anything can throw. Либо SPARK верифицировал критичный к производительности код, и это даёт мандат на отключение runtime проверок в этой части кода. Как в libsparkcrypto. Или вот ещё, 13й слайд.
Какого-то компромисса здесь не просматривается. Архитекторы Rust, мне кажется, промахнулись, пытаясь нащупать таковой. Чтоб самый обычный плюс и минус, которые везде, были спусковыми крючками апокалипсиса, ну такое. Мне кажется, потенциальным программистам на Rust надо лучше объяснять, в какую петлю они суются.
TargetSan
Вообще-то нет. Перечитайте. Обычные плюс и минус в дебаге при переполнении выдают ассёрт, а в релизе работают как wrapping операция. Паника будет только при делении на ноль.
OCTAGRAM
wrapping в релизе был чем-то настолько немыслимым, настолько редким специальным случаем, что я этот вариант даже не принял к рассмотрению. Нет проверок на числах — нет чисел. Нет чисел — нет программы.
TargetSan
Зато Unchecked_Deallocation это супер современно.
red75prim
> Нет проверок на числах — нет чисел. Нет чисел — нет программы.
Не очень убедительно. Чем это утверждение отличается от: «SPARK не обеспечивает отсутствие deadlock'ов на multicore машинах. Есть deadlock'и — нет программы»?
Арифметика по модулю на процессорах — это умолчание. Если алгоритм не учитывает этого, то вылет исключения по переполнению ничем не поможет корректно обработать входные данные (или сломает всё, как случилось с Arian 5). Невылет исключения конечно тоже ничем не поможет. Так что дело тут не в арифметике по модулю, а в средствах верификации. И, да, SPARK тут превосходит Rust.
netch80
> Арифметика по модулю на процессорах — это умолчание.
1) Не везде и не всегда.
S/360 и потомки: флаг в PSW по переполнению генерировать исключение.
MIPS: различие команд add (исключение при знаковом переполнении) и addu (нет такого).
Это только самые яркие примеры.
Ну а в остальных обычно есть средства немедленно проверить на переполнение (как jo в x86), как раз для случая, когда надо проверять.
2) А с каких это пор «умолчание в процессорах» стало аргументом для безопасного языка? На уровне процессора ведь нет (если мы не про iAPX432, AS/400, и т.п.) защиты памяти, защиты const-переменных от изменения, и многого другого, что должно быть в языке. Это просто не его дело. А дело языка — использовать процессор надлежащим образом, а где нужно — и границы массива проверить, и писать в чужую память не давать, и переполнение проверить.
> Так что дело тут не в арифметике по модулю, а в средствах верификации.
И что будет, если верификация откажется принимать код, потому что не осилит проверку? А такое происходит сплошь и рядом.
Ошибка по переполнению — это простой надёжный метод обеспечить гарантию неподстановки неверного результата операции. Поэтому и должно использоваться по умолчанию.
(Если компилятор по анализу программы может убрать эту проверку — то пусть убирает. В выхлопе какого-нибудь clang это происходит постоянно. Но если не уверен — оставляет, и это хорошо.)
netch80
> Следовательно, бросить исключение из оператора сложения мы не можем. Иначе был бы C++ «anything can throw».
1) Есть альтернативы, например, в виде флага, который ставится в 1 по ошибке, и который можно проверять (точно так же, как по стандарту IEEE754 это затребовано task-local для плавучки). Можно придумать переопределение режима и флага для своего куска кода, не обязательно в TLS, годится любая указанная переменная.
2) Вообще, позиция отрицания «anything can throw» это перегиб даже больший, чем предыдущее активное введение структурных исключений во все новые языки. И паника, которая по умолчанию что-то печатает, по такому событию — тоже.
Можно было бы подумать в эту сторону, но не отвергать исключения совсем.
> К тому же, проверка каждой операции приводила бы к оверхеду. Результатом был бы жуткий срач.
При нормальном современном интеллекте компилятора большинство проверок такого рода будет устранено. Если у вас, грубо говоря, for (i = 0; i < 100; ++i), и код не меняет i в теле цикла, то результат ++i проверять не нужно. Это сейчас умеет LLVM из коробки. А если какие проверки и останутся — то, значит, им тут место.
Про срач — если, как у современных компиляторов, код веток «что-то пошло не так» выносится отдельно, то, да, это будет обширнее, чем если бы проверка не делалась, но отнюдь не «ужас-ужас».
> Для тех, кому нужна предсказуемая арифметика, у каждого целочисленного типа Rust есть набор методов checked/saturating/wrapping/overflowing.
Ну вот пока подход «для тех, кому нужна», а не по умолчанию… как говорил один мой знакомый, security бывает двух уровней — high и «няхай». Впрочем, кто хочет смягчить защиту и уверен в этом — пусть язык даст ставить атрибут на кусок кода.
С другой стороны, что в Rust начали вообще предоставлять подобные средства «из коробки» — уже само по себе грандиозный прогресс после полувека наплевательства.
AngReload
Тут у Rust'a много хороших штук.
Компилятор следит за стилем наименования переменных, жалуется на лишние скобки, есть тулза для автоформатирования, числа с плавающей точкой нужно писать с точкой. Не получится забыть объявить переменную, нельзя сравнить разные типы, если в условии написать = вместо == то выдаст ошибку типа. Наверно, сюда ещё можно отнести отсутствие перегрузки функций, автовывод типов, макросы работающие не на строках, а с AST, иммутабельные по умолчанию переменные, предупреждения об неиспользуемых переменных и мутабельности. Ну что вспомнил, в целом язык более прозрачный чем все другие что я видел, а компилятор пытается помочь избежать ошибок.