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" без уникального позиционирования.

В репозитории представлено детальное сравнение решений 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.

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

В 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.