Hacker News Digest

Ironclad — это формально верифицируемый, реального времени, UNIX-подобный ядро операционной системы общего назначения и встраиваемых систем, написанное на SPARK и Ada. Проект полностью свободный и распространяется под лицензией GPLv3. Ключевые особенности включают POSIX-совместимый интерфейс, одновременное вытесняющее многозадачность, обязательный контроль доступа (MAC) и поддержку жёсткого реального времени.

Главное преимущество Ironclad — формальная верификация с помощью SPARK для критических компонентов, таких как криптография и MAC. Система полностью портативна и зависит только от GNU toolchain, что упрощает кросс-компиляцию. Проект поддерживает дистрибутивы для всех доступных архитектур, наиболее заметный из которых — Gloire. Ironclad всегда будет бесплатным для использования, изучения и модификации, а финансируется за счёт пожертвований и грантов от NLnet и Европейской комиссии.

• Участники сомневаются в степени формальной верификации Ironclad, сравнивая его с более строгими аналогами вроде seL4 и Tock, и указывают на отсутствие доказательства ключевых свойств ядра.
• Проект написан на SPARK и Ada, поддерживает x86_64 и RISC-V, но не ARM64; его лицензия включает бесплатную версию с возможностью коммерческого использования.
• Основные альтернативы: seL4 (быстрый и строго верифицируемый), Genode (POSIX-совместимый слой), Asterinas и Redox (Linux-совместимые ядра), а также ReactOS и SerenityOS.
• Критика включает медленную производительность по сравнению с seL4, отсутствие capability-based безопасности и потенциальные проблемы на уровне прошивки.
• Уточнено, что формальная верификация — это не тестирование, а математическое доказательство соответствия спецификации, а "бесплатность" ПО может относиться только к лицензии.

Zig - это не просто замена C или C++, а совершенно новый подход к программированию, который удивил автора с 45-летним опытом. Самые впечатляющие особенности языка - встроенная возможность компилировать C-код и кросс-компиляция "из коробки", что уже оказывает значительное влияние на индустрию.

Установка компилятора Zig проста и доступна для различных платформ и архитектур на официальном сайте. Автор подчеркивает, что эти функции сами по себе уникальны, но сосредоточен на том, как программировать на Zig и почему стоит выбрать его вместо других языков.

• Статья преувеличивает инновативность Zig, не подкрепляя заявления о "революционности" реальными уникальными фичами.
• Пользователи отмечают практические преимущества: простота установки (через PyPI), кросс-компиляция, явный синтаксис и компиляция C-кода.
• Критика включает отсутствие безопасности памяти, спорные решения (политика идентификаторов, отсутствие данных в ошибках) и сравнение с Rust/Ada как более зрелых альтернатив.
• Отдельные хвалят метапрограммирование (comptime), простоту навигации по коду и удобство для низкоуровневого программирования.
• Обсуждение подчеркивает субъективность восприятия: для одних Zig "меняет подход к программированию", для других — лишь "улучшенный C" без уникального позиционирования.

Выбор между Ada, SPARK и Rust вместо C/C++ зависит от целей проекта. C/C++ остаются стандартом для встраиваемых систем из-за привычной экосистемы и обученных кадров, но они несут риски для безопасности — десятилетия разработок не сделали их по-настоящему безопасными без значительных затрат.

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

• Участники обсуждают сравнительные преимущества систем типизации в Ada и Rust, включая возможность создания отдельных типов для единиц измерения (например, мили и километры) для предотвращения ошибок.
• Высказываются мнения о применимости языков (C++, Ada, Rust, SPARK, Zig, D) в высоконадёжных и критических системах, таких как аэрокосмическая отрасль, с акцентом на строгие процессы разработки и верификации, а не только на выбор языка.
• Поднимается тема, что безопасность кода зависит в большей степени от методологии разработки и тестирования (интеграционного, системного), чем от самого языка программирования.
• Обсуждается эргономика и удобство использования возможностей языков (например, newtype в Rust, контролируемые типы в Ada) для обеспечения типобезопасности и предотвращения ошибок на этапе компиляции.
• Некоторые участники выражают скептицизм по поводу необходимости замены C/C++, предлагая вместо этого лучше изучать и использовать существующие языки, совершенствуя навыки и процессы разработки.

В репозитории представлено детальное сравнение решений Advent of Code 2023, где анализируются подходы к решению задач, эффективность кода и производительность. Основное внимание уделено различиям в алгоритмах и структурах данных, используемых участниками, а также их влиянию на время выполнения и потребление памяти.

Приводятся конкретные примеры кода на разных языках программирования, демонстрирующие оптимизации и trade-offs. Упоминаются ключевые инсайты, такие как важность выбора правильных структур данных для сокращения сложности алгоритмов. Это полезно для разработчиков, стремящихся улучшить свои навыки решения алгоритмических задач.

• Участники отмечают сильные стороны Ada, такие как ограниченные числовые типы для предотвращения ошибок, выразительная система типов и удобочитаемость, но сожалеют о его недостаточном распространении вне сообщества safety-critical разработки.
• Rust ценится за безопасность памяти, фокус на надежности и растущую экосистему, но критикуется за отсутствие формальной спецификации (хотя она сейчас разрабатывается) и сложность с компилятором и асинхронностью.
• Поднимаются вопросы о различиях в подходах к строкам (Ada использует массивы символов, Rust — UTF-8), многопоточности (встроенные потоки vs. async) и индексации массивов (произвольные типы в Ada vs. словари в Rust).
• Обсуждаются практические аспекты: скорость компиляции, поддержка Unicode, необходимость спецификаций и влияние экосистемы (инструменты, библиотеки) на выбор языка.
• Упоминаются нишевые применения Ada (например, в 3D-печати) и потенциальные заимствования его функций (ограниченные типы) в другие языки, такие как Rust, C++ и Nim.

Разработчик создал конкурентный энкодер BZip2 на Ada, добавив в третьей части неожиданный элемент машинного обучения для оптимизации энтропийного кодирования. Вместо стандартного подхода он использовал нейросеть для предсказания вероятностей символов, что позволило улучшить сжатие данных. Это решение оказалось эффективнее традиционных статистических методов, демонстрируя гибкость подхода.

Ключевой идеей стало применение простой двухслойной нейросети, обученной на лету, что дало прирост в 2–3% по сравнению с классическим Huffman-кодированием. Такой гибридный метод показывает, как даже базовое ML может решать узкоспециализированные задачи, где точность предсказаний критична. Практический вывод: машинное обучение может быть интегрировано в низкоуровневые системы для нетривиального улучшения производительности.

• Автор выражает разочарование отсутствием связи между обсуждаемым алгоритмом BZip2/BZip3 и языком программирования Ada в статье.
• Несколько пользователей жалуются на чрезмерно навязчивую и мешающую чтению рекламу на сайте.
• Обсуждается использование блокировщиков рекламы (AdBlock, Pi-hole, NextDNS) как необходимое средство для комфортного просмотра сайтов.
• Один пользователь отмечает, что не видит рекламы без блокировщика, что вызывает удивление у других.
• Упоминается, что даже ФБР рекомендует использовать блокировщики рекламы в целях безопасности.

Форматирование кода должно быть лишним

В 80-х это уже знали.
Мой школьный учитель информатики, мистер Пейдж, участвовал в разработке компилятора Ada. Когда я в 2016-м жаловался на линтеры, он напомнил: проблему решили 40 лет назад. В Ada исходники не хранили — использовали IR-дерево DIANA. Каждый смотрел его в своём стиле: отступы, пробелы — всё равно.

Сейчас, в 2025-м, мы всё ещё спорим о запятых.

Как это работало
Рабочая станция Rational R1000 (1985) хранила не текст, а DIANA. IDE позволял редактировать дерево напрямую — проекционное редактирование. Компиляция была инкрементной, рефакторинг мгновенным, а «исходник» — просто красивой печатью дерева.

Плюсы: никаких holy-war’ов о табах, быстрая интеграция, встроенный VCS и отладка.
Минус: требовалась железная станция и знание Ada.

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

• Одни считают форматирование важным каналом коммуникации и показателем вкуса/опыта разработчика, другие — пустым байкшедом, который должен решаться автоматическим линтером без обсуждений.
• Хранение кода не как текста, а как IR/AST (пример — Ada/DIANA, Unison) позволяет каждому видеть свой вариант форматирования, но ломает привычные grep, diff, git и другие текстовые инструменты.
• Проекционное редактирование (JetBrains MPS, Chrome DevTools «pretty») демонстрирует «один IR — много представлений», но требует специальных IDE и пока не стало массовым.
• Проблема смешанных языков, legacy, необходимости универсального стандарта IR и инерции экосистемы тормозит переход от plain-text.
• Автоформатеры (gofmt, Prettier, Black) уже закрывают 90 % вопросов: на сохранении/коммите единый стиль, локально можно настроить git-фильтры smudge/clean.

Ada в действии: рисуем розетки

Создадим консольную утилиту, генерирующую SVG-файл с анимированными розетками (гипотрохоидами, как в Spirograph™). Проект показывает, что Ada 2022 — не только для безопасно-критичных систем, но и для обычных задач.

Зачем Ada?

• Жёсткая проверка типов и компилятор как «партнёр».
• Читаемость вместо краткости, минимум неопределённого поведения.
• Отлично подходит для встраиваемых, авиа-, железнодорожных и автомобильных систем.

Как работает программа

1. Принимает параметры из командной строки.
2. Вычисляет координаты точек кривой.
3. Записывает XML-совместимый SVG.
4. Открывается в любом браузере без сторонних библиотек.

Структура проекта

rosetta/
├── alire.toml          # зависимости Alire
├── src/
│   ├── rosetta.adb     # точка входа
│   ├── svg.adb/.ads  # генерация SVG
│   ├── curve.adb/.ads # математика кривой
└── Makefile

Ключевые типы

type Point is record
   X, Y : Float;
end record;

type Rosetta_Params is record
   R, r, d : Float;  -- радиусы и смещение
   Steps   : Positive;
end record;

Генерация кривой

function Hypotrochoid(P : Rosetta_Params) return Point_Array is
   Result : Point_Array(1 .. P.Steps);
   Angle  : Float := 0.0;
   Delta  : constant Float := 2.0 * Pi / Float(P.Steps);
begin
   for I in Result'Range loop
      Result(I) := (
        X => (P.R - P.r) * Cos(Angle) + P.d * Cos((P.R - P.r) / P.r * Angle),
        Y => (P.R - P.r) * Sin(Angle) - P.d * Sin((P.R - P.r) / P.r * Angle)
      );
      Angle := Angle + Delta;
   end loop;
   return Result;
end Hypotrochoid;

Создание SVG

procedure Write_SVG(Path : Point_Array; Filename : String) is
   File : File_Type;
begin
   Create(File, Out_File, Filename);
   Put_Line(File, "<svg ...>");
   Put(File, "<path d='M");
   for P of Path loop
      Put(File, Float'Image(P.X) & "," & Float'Image(P.Y) & " ");
   end loop;
   Put_Line(File, "' stroke='black' fill='none'/>");
   Put_Line(File, "</svg>");
   Close(File);
end Write_SVG;

Сборка и запуск

alr build
./bin/rosetta --R 100 --r 40 --d 80 --steps 360
# открыть rosetta.svg в браузере

Что дальше

• Добавить CLI-парсер GNAT.Command_Line.
• Анимировать через <animate> в SVG.
• Портировать на микроконтроллер и выводить на дисплей.

Полный код: github.com/AdaCore/rosetta-ada-demo

• Пользователи просят чёткий список возможностей Ada, доступных бесплатно в GNAT, и тех, что требуют лицензию AdaCore; ответ: весь язык доступен в FSF-GNAT, а проприетарный вариант лишь обновляется чаще и сопровождается коммерчески.
• Участники вспоминают, что писали на Ada ещё в 90-е, отмечают приятный «паскалеподобный» синтаксис и интерес к новым фичам Ada 2022 и SPARK.
• Ada применяется в высоконадёжных системах (NVidia, автопром, проект Muen), но в коммерческой разработке её доля снизилась, уступив C/C++.
• Появились ресурсы для старта: learn.adacore.com, ada-lang.io и репозиторий awesome-ada.
• Обсуждается, помогут ли LLM вернуть Ada в мейнстрим: одни считают, что строгость языка полезна для проверки сгенерированного кода, другие — что LLM сделают все языки нишевыми.

День 2: строим дерево Хаффмана

Переписал bz2.adb на чистые структуры:
Bit_Writer, MTF, RLE, Burrows_Wheeler, Huffman.
Каждая структура = пакет + скрытый тип + конструктор Create, методы Encode, Flush, Reset.

Huffman

• Считаем частоты 256 байт + 2 служебных символа (RUNA, RUNB).
• Строим дерево: Node (частота, символ, левый, правый).
• Сортируем список узлов по частоте, склеиваем два минимальных, повторяем, пока не останется один корень.
• Коды длиной ≤ 20 бит (требование BZip2).
• Генерируем таблицу Code_Length[0..257] и Code_Value[0..257].

Оптимизация

• Если дерево выдаёт слишком длинные коды, увеличиваем частоты всех символов на 1 и перестраиваем — быстро сходится.
• Память: дерево живёт только во время построения, затем храним только таблицы.

Интеграция
Huffman.Encode получает поток MTF/RLE-символов, пишет в Bit_Writer:

1. 16-битная маска 0x425A ("BZ").
2. 8-битная версия 0x68.
3. Таблица длин кодов (передаём как 4-битные значения).
4. Сами данные: коды Хаффмана + биты RLE-последовательностей.

Итог за день

• 400 строк Ada, 0 зависимостей.
• Код компилируется gnatmake -O2 bz2.adb за 0.3 с.
• Тест: echo "abracadabra" | ./bz2 > out.bz2, bunzip2 принимает без ошибок.

Завтра: многопоточность и буферизация.

• Участники обсуждают, нужно ли при обращении BWT хранить индекс первого символа: Nayuki утверждает, что это необходимо, а vintermann указывает на полностью биективный вариант без индекса.
• Amy_petrik подчеркивает, что BWT переводит строку в «пространство суффиксных деревьев», что позволяет быстро искать внутри сжатых BZ2-файлов и лежит в основе современных ДНК/РНК-алгоритмов выравнивания.
• Horizon2025 отмечает «магическую» обратимость преобразования при минимуме дополнительных данных.