Hacker News Digest

Архив Эдсгера Дейкстры содержит более тысячи его неопубликованных рукописей, известных как "EWDs", которые он рассылал десяткам получателей на протяжении более 40 лет. Дейкстра, один из основоположников компьютерных наук (1930-2002), внёс фундаментальный вклад в алгоритмы, языки программирования, операционные системы и формальную верификацию, за что получил высшую награду ACM - премию Тьюринга. Большинство его работ остались недоступными для широкой публики, пока не были оцифрованы и представлены на этом сайте в виде PDF-документов.

Исходные материалы, включая дневники и переписку, хранятся в Техасском университете. Архив включает несколько индексов для поиска, а также растущее количество транскрибированных текстов и переводов на разные языки. Дейкстра часто возвращался к уже обсуждавшимся темам, предлагая новые взгляды или более точные формулировки, что отражено в системе перекрёстных ссылок между документами.

• Дискуссия охватывает темы от индексации массивов до философии обучения программированию, включая ссылки на конкретные эссе и письма Дейкстры.
• Участники обмениваются ссылками на тексты Дейкстры, обсуждают его взгляды на обучение программированию, индексацию и стиль написания кода.
• Обсуждение затрагивает влияние Дейкстры на современную практику разработки ПО, включая дискуссии о том, как его идеи могут быть применимы или неприменимы в современном контексте.
• Участники также обсуждают влияние Дейкстры на современные языки программирования и стиль написания кода, включая дискуссии о том, как его идеи могут быть применимы в современной разработке ПО.
• Некоторые участники также обсуждают, как идеи Дейкстры могут быть использованы в обучении новых программистов и как его идеи могут быть применимы в современной разработке ПО.

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 безопасности и потенциальные проблемы на уровне прошивки.
• Уточнено, что формальная верификация — это не тестирование, а математическое доказательство соответствия спецификации, а "бесплатность" ПО может относиться только к лицензии.

LISP просуществовал 21 год к 1980 году, потому что представляет собой приблизительный локальный оптимум в пространстве языков программирования. Маккарти отмечает, что язык накопил некоторые "балластные" элементы, которые следует устранить, и упустил возможности для улучшений. Языку помогло бы совместное обслуживание, особенно в создании и поддержке библиотек программ. Компьютерно проверяемые доказательства корректности программ теперь возможны для чистого LISP и некоторых расширений, но для полного использования математической основы языка требуется больше теории и упрощения самого языка.

В примечании 1999 года Маккарти отмечает, что его взгляды 1980 года в основном соответствуют текущим. Основная идея заключается в том, что LISP, несмотря на свою долговечность, нуждается в очистке от лишних элементов и улучшении для раскрытия его полного потенциала, особенно в области формальных доказательств корректности программ.

• Обсуждение показало, что Lisp и его диалекты всё ещё живы, но в нишевых формах: от Clojure на JVM до CHICKEN Scheme, компилирующего в C.
• Участники отмечают, что язык остаётся мощным инструментом, но его экосистема и сообщество сильно сократились, и нет признаков возвращения в мейнстрим.
• Некоторые подчеркнули, что Lisp-языки всё ещё важны для AI-исследований, генетического программирования и метапрограммирования.
• Сообщество отметило, что популярность языка упала не из-за технических причин, а из-за смены парадигмы в разработке ПО от символического AI к нейронным сетям и статистическому программированию.

Автор объясняет, что Isabelle сознательно отказалась от объектов доказательств, которые являются неотъемлемой частью обычных теорий типов. Это сделано потому, что объекты доказательств не нужны и занимают много места. Вместо этого Isabelle использует архитектуру LCF, где проверка типов осуществляется в языке реализации, а не в логике, что гарантирует легитимность шагов доказательства. Robin Milner имел это фундаментальное понимание 50 лет назад.

Лоуренс Полсон рассказывает о своем опыте работы с AUTOMATH и Martin-Löf type theory. Первоначально Isabelle была реализацией Martin-Löf type theory, которая до сих пор включена в дистрибутив как Isabelle/CTT. Однако автор переключился на более общий подход, вдохновленный AUTOMATH - "большим рестораном, который обслуживает любую кухню". В итоге Isabelle/HOL стала доминирующей, хотя де Брёйн не одобрял растущую мощь теорий типов и презирал теорию множеств.

• Обсуждение показало, что вопрос не в «плохих» зависимых типах, а в том, что они не нужны для большинства задач и не оправдывают свою сложность.
• Участники обсуждали, что отсутствие зависимых типов не мешает Isabelle/HOL доказать критически важные части математики, и что вместо этого важнее автоматизация и библиотеки.
• Сообщество отметило, что даже в языках без зависимых типов можно выразить «матрица 10×5 из float32», если размеры известны на этапе компиляции, и что это покрывает большинство практических случаев.
• Несколько участников поделились личным опытом, что попытка использовать зависимые типы в продакшене привела к тому, что команды отказались их использовать из-за кривой кривой обучения и отсутствия инструментальной поддержки.
• В итоге автор статьи подытожил, что выбор между зависимыми типами и другими системами типов часто сводится к личным предпочтениям и доступным инструментам, а не к объективным преимуществам.

Cuq — это фреймворк, преобразующий MIR (промежуточное представление Rust) в Coq для формальной семантики и верифицированного перевода Rust-ядер GPU. Проект нацелен на PTX (язык ассемблера NVIDIA) и обеспечивает математически строгую основу для GPU-программирования на Rust.

Фреймворк позволяет формально доказывать свойства GPU-кода и обеспечивает верифицированный перевод из Rust в PTX. Это критически важно для безопасности и надежности вычислений на GPU, где ошибки могут иметь серьезные последствия. Cuq заполняет пробел между высокоуровневым Rust-кодом и низкоуровневым GPU-исполнением, предоставляя формальные гарантии корректности преобразований.

• Проект, который переводит MIR Rust в Coq для формальной верификации ядра CUDA, вызвал бурную дискуссию из-за имени «cuq».
• Участники спорят, звучит ли название как «кук» или «кью-кью»; критика имени превратилась в обсуждение культурных различий.
• Некоторые предлагают переименовать проект в «rocuda», «rocq» или «rocq», чтобы избежать нежелательных коннотаций.
• Автор отвечает, что имя строится на словах CUDA и Coq, и что он не осознавал двусмысленность; вопрос о переименовании остаётся открытым.
• Несмотря на спор, техническая ценность проекта в том, что он может формально верифицировать параллельные вычисления и уменьшить гонки за счёт формального доказательства корректности.

Формализация математики в системах вроде Lean полезна не только для обнаружения ошибок, как считают многие. Автор статьи, работающий над формализацией доказательств в Lean для учебника Тана по реальному анализу, проводит параллель с TypeScript: хотя статическая типизация в первую очередь нацелена на поиск багов, её истинная ценность в другом. TypeScript обеспечивает поддержку инструментов разработчика, служит языком проектирования и даёт немедленную обратную связь при написании кода.

Аналогично, формализация математики предлагает преимущества, выходящие за рамки проверки корректности. Во-первых, она создаёт мощную экосистему инструментов: навигацию по определениям, автоматическую генерацию документации, поиск и рефакторинг. Во-вторых, позволяет анализировать мета-математические тренды, визуализировать графы зависимостей теорем и автоматически находить альтернативные пути доказательств. В-третьих, внедрение системы контроля версий для математических результатов сделает эволюцию математических истин более управляемой. Цена такого прогресса — необходимость доказывать множество тривиальных утверждений, которых в неформальной математике обычно избегают.

• Lean и другие инструменты формализации делают математику доступной для «хоббистов», но не решают фундаментальной проблемы: формальная проверка не заменяет математическое мышление и не гарантирует, что вы доказываете именно то, что задумали.
• Сообщество Lean-математиков стремится к полной формализации всей математики, но пока это выглядит как попытка «сделать ее удобной для компьютера»; критики считают, что это отвлекает от сути исследований и не решает проблему обучения доказательствам.
• Теоретически, формальные доказательства должны быть полезны для обучения, но на практике большинство математиков не используют формальные доказательства как учебный материал.
• Использование формальных верификаторов для обучения может привести к тому, что студенты будут полагаться на компьютер вместо развития интуиции.
• Сообщество формальных верификаторов стремится к тому, чтобы их инструменты были доступны для математиков, но они не решают проблему, что делает доказательства формальными — это требует математического мышления, которое не может быть заменено компьютером.

Несмотря на формальную верификацию, код может содержать ошибки. Одна из причин — несоответствие спецификации: доказательство может подтверждать корректность кода относительно формальной спецификации, но если сама спецификация неполна или неточно отражает реальные требования, код может работать некорректно.

Например, в случае с leftpad, многие реализации были формально верифицированы относительно свойства «длина результата равна максимуму из n и длины s», но это не гарантирует, что результат будет визуально корректным при использовании Unicode-символов.

Другая проблема — ошибки в самом инструменте верификации, хотя такие случаи редки.

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

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

• Обсуждение показало, что формальная верификация кода не покрывает аппаратные сбои и ограничения окружения, а также не решает проблему валидации требований пользователя.
• Участники подчеркнули, что доказательство корректности кода не защищает от ошибок в спецификации, а также не покрывает такие факторы как переполнение целочисленных типов и другие архитектурные ограничения.
• Была затронута тема различия между верификацией (verification) и валидацией (validation), где первое касается соответствия кода спецификации, а второе — решаемости реальной задачи.
• Обсуждение подняло вопрос о том, что формальные методы не покрывают такие аспекты как отказ оборудования, влияние космических лучей и другие факторы окружения, что делает их менее полезными в контексте безопасности.
• Участники также обсудили, что даже при наличии формальной верификации, остаются риски, связанные с человеческим фактором, так как спецификация может не отражать реальные требования пользователя.

Litex — это формальный язык программирования, который можно освоить всего за 1–2 часа благодаря минималистичному синтаксису и чёткой структуре. Он предназначен для обучения основам формальных систем и логики, сохраняя при этом практическую полезность. Язык включает всего несколько ключевых конструкций, что снижает порог входа для новичков.

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

• Обсуждение нового формального языка Litex для машинной проверки рассуждений, который позиционируется как простой и интуитивно понятный, даже для новичков без математического бэкграунда.
• Критика и скептицизм по поводу заявлений автора, в частности, о скорости обучения и легкости формализации по сравнению с Lean 4, а также вопрос о том, как реализована проверка доказательств.
• Обсуждение технических деталей языка: необходимость явно объявлять аксиомы (например, транзитивность), использование ключевого слова have для проверки существования объектов.
• Подняты вопросы о возможной путанице с уже существующим проектом LiteX (аппаратное описание на Python) и о том, написан ли README проекта с помощью ИИ.
• Отмечается, что автор, вероятно, не является носителем английского языка, что могло привести к некоторым неточностям в формулировках и сложностям в понимании.

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

Такой прогресс открывает перспективы широкого использования инструментов вроде Lean без необходимости глубоких экспертных знаний, что может ускорить верификацию критических систем, криптографии и компиляторов. Практический совет: попробуйте сами инструменты вроде Claude Code или Gemini CLI на знакомых задачах — это обойдётся примерно в $20–100 в месяц.

• Участники обсуждают потенциал LLM (особенно Claude Code) в генерации формальных доказательств и кода с использованием инструментов вроде Lean, отмечая, что ИИ часто успешно справляется с первой частью задачи, но испытывает трудности с завершающими, самыми сложными этапами.
• Подчеркивается фундаментальная проблема: сложность не в написании кода, а в создании точных и корректных спецификаций и требований, что является ключевым для формальной верификации и доказательства правильности программ.
• Высказывается мнение, что сочетание генеративных ML-моделей с формальными методами — многообещающий путь вперед, так как LLM снижают усилия на реализацию, а формальные методы — на проверку, компенсируя слабые стороны друг друга.
• Обсуждаются практические сложности: необходимость жесткого контроля за выводом ИИ, риск получения ложных доказательств, которые лишь выглядят корректно, и важность эмпирической валидации результатов, сгенерированных ИИ.
• Отмечается, что архитектурные решения и изменяющиеся требования часто делают формальные доказательства непрактичными для большинства реальных проектов, где код не статичен, а правильное абстрагирование и разделение ответственности важнее тотальной корректности.

%PDF-1.5  
9 0 obj  
stream  
…сжатое содержимое…  
endstream  
endobj  

54 0 obj  
stream  
…сжатое содержимое…  
endstream  
endobj  

102 0 obj  
stream  
…сжатое содержимое…  
endstream  
endobj  

127 0 obj  
stream  
…сжатое содержимое…  
endstream  
endobj  

• Большинство участников считают, что Ферма либо ошибся, либо пошутил: за три десятилетия он не записал «элегантное» доказательство, а все последующие попытки найти простое решение провалились.
• Обсуждаемый документ — это лишь «чертеж» (blueprint) будущего формализованного доказательства Великой теоремы Ферма в системе Lean; само доказательство займёт ещё несколько лет.
• Ключевой мотивацией формализации называют повышение надёжности: компьютер сможет полностью проверить громоздкое доказательство, исключив человеческие ошибки.
• Участники обеспокоены долговечностью кода и спрашивают, как предотвратить «захват» задач бездействующими участниками и избежать дублирования работы.
• Для массового использования Lean требуются учебные материалы и «текстбы» на его основе; уже появляются книги и курсы, включая упражнения Теренса Тао.