Hacker News Digest

Bend 2 позиционируется как язык для эпохи AI-кодинга: человек пишет «законы», а ИИ генерирует реализации и доказательства, которые компилятор проверяет на корректность. Однако автор статьи указывает, что в демонстрации Bend для простого свойства — что игрок никогда не коснётся флага и не выиграет игру — требуется 58 строк кода для формулировки законов и целых 442 строк для их доказательства ИИ. Это выглядит избыточно, особенно если сравнить с существующими подходами в формальной верификации.

Автор показывает, что эквивалентную задачу можно решить гораздо проще на SPARK — языке с встроенной поддержкой формальной верификации. После указания типов, инвариантов и условий, достаточно запустить GNATprove, который подтверждает корректность программы за 12 проверок без необходимости писать громоздкие доказательства вручную или через ИИ. Это демонстрирует, что Bend изобретает велосипед, игнорируя десятилетия исследований в области формальной верификации, термины которой даже не упоминаются на его сайте или в коде.

Основная проблема — не в самом Bend, а в явлении «vibe-coding»: когда разработчик, вдохновлённый возможностями ИИ, сразу приступает к созданию сложной системы (языка, компилятора), не проверив, существует ли уже эффективное решение. ИИ с радостью поможет построить что-то с нуля, но не подскажет, что 99% работы уже сделано и доступно для переиспользования. В результате получается решение, которое работает, но является избыточным и устаревшим по сравнению с текущим состоянием области. Это не просто плохой дизайн — это системная рискованная практика, когда отсутствие предварительного исследования приводит к изобретению хуже существующего.

Обсуждение опровергает утверждение статьи о незнании автором Bend формальной верификации: он публиковал работы и доклады по этой теме за последние 7–8 лет, включая реализацию Cedille Core и выступления на DevCon. Критика Bend за использование 442 строк доказательства некорректна: современные системы вроде Isabelle/HOL и Lean имеют доказательства в десятки тысяч строк — размер не показатель неэффективности. Сравнение Bend с GNATprove некорректно: SMT-решатели автоматически генерируют доказательства, но не масштабируются на сложные системы, тогда как Bend пытается использовать LLM для генерации символьных доказательств — это ново. Vibe-coding позволяет быстро создавать рабочие решения, но мешает осознать, что существуют более эффективные подходы, особенно без предварительного исследования. Проблема не в Bend, а в том, что LLM не предупреждают о существующих решениях — пользователь должен сам запрашивать prior art, иначе повторяет уже решённые задачи. Совет: перед созданием языка или фреймворка стоит начинать с запроса к LLM о существующих решениях — это экономит время и предотвращает повторение известных подходов. Формальная верификация не требует упрощения синтаксиса — её сложность обусловлена природой задачи, и LLM могут помочь управлять этой сложностью, а не заменять её. Критика Bend как «ужасно устаревшего» — это стратегический соломенный человек: автор не игнорирует поле, а пытается сделать его доступнее, что требует иного подхода к UX, а не к теории. Компилятор Bend, написанный на 99% ИИ и не аудитированный, — серьёзный риск, но он не опровергает идею языка, а лишь указывает на необходимость более осторожной реализации. Пользователи не требуют идеальных решений — если работоспособное решение решает их задачу, то 442 строки доказательства не являются препятствием, особенно в корпоративной среде. Совет: лучший язык для взаимодействия с LLM — не компилируемый, а интерактивный, как Lisp, потому что доказательства требуют итеративной корректировки, а не однократной генерации. Попытки создать новый язык из-за недовольства существующими часто приводят к худшим результатам, если не основаны на глубоком понимании предметной области и её исторического контекста. Самая большая опасность vibe-coding — уверенность в том, что сгенерированное решение уникально и лучше, тогда как оно часто является переоткрытием уже существующего. Критики Bend не провели базовое исследование о его авторе — это пример vibe-coding в критике: судят по внешнему виду, а не по содержанию. Совет: вместо осуждения попыток инноваций следует фокусироваться на том, как сделать их более осознанными: исследование, прозрачность и признание существующих работ — ключ к уважаемым проектам.

Гемини 3.7 Flash — новое поколение «рабочей лошадки» от Google, созданное для сложного программирования и агентных сценариев. За три недели после релиза 3.6 Flash компания представила модель с существенно улучшенным пониманием кода, точностью генерации и способностью работать с длинными цепочками задач. На тестах FrontierCode 1.1 точность выросла с 34,4 % до 43,6 %, а в DeepSWE v1.1 — с 49,0 % до 65,3 %. В веб‑разработке 3.7 Flash генерирует полноценные приложения и UI‑компоненты из меньшего числа промптов, а на Arena.ai WebDev Arena набрал Elo 1588 против 1538 у предшественника.

Особенно заметны рост точности в обработке тяжёлых документов: на бенчмарке GDP.pdf показатель вырос с 22 % до 34 %, а в AutomationBench — с 17 % до 30,4 %. Стоимость остаётся вдвое ниже, чем у 3.6 Flash (0,75 $/млн входных и 3,75 $/млн выходных токенов), а новая версия лучше адаптируется к подводным камням, уточняет намерения пользователя и требует меньше ручного контроля. Теперь разработчики могут использовать её в Google AI Studio, Android Studio и через Gemini Enterprise, а обычные пользователи — в Spark внутри приложения Gemini.

Gemini 3.7 Flash лидирует по скорости и низкой задержке, что критично для интерактивных сценариев (например, Google AI Mode), но страдает от сложного парсинга «мыслей», академичного стиля ответов и неконкурентоспособной долгосрочной цены — после 2026 года тариф удваивается, при этом модель к тому времени устареет. Пользователи отмечают: - Модель лучше подходит для агентных задач и быстрых итераций, но слаба в сложном кодинге и рефакторинге — уступает GPT-5.6 Luna, DeepSeek и Opus. - Вывод требует значительной очистки от внутренних монологов, усложняя интеграцию. - Стиль ответов стал менее интуитивным, вероятно, из-за RLVR-тренировок. - Галлюцинации и ложные утверждения сохраняются в серии Flash (3.1–3.7), снижая доверие по сравнению с Claude или Sol. - Генерация SVG сломана в Firefox и Chrome из-за невалидных фильтров — проблема кросс-браузерной совместимости. - В image-to-html уступает Opus 5, но сопоставима с Grok 4.6. - Интеграция в Android-ассистента ухудшила UX: модель галлюцинирует инструкции и отказывается выполнять простые команды. - Google Cloud: запутанная номенклатура (Gemini, Anti-gravity, Vertex) и сложная регистрация CLI-инструментов отталкивают разработчиков. - Для специфических задач (анализ рынков на Rust) Stepfun AI Step-3.5-Flash дешевле и эффективнее. - AA-метрика выросла за счёт увеличения токенов вывода, а не качества — экономика использования изменилась. - Качество ответов («vibes») остаётся важнее бенчмарков: пользователи предпочитают Claude за стиль, несмотря на цифры. Споры о целесообразности: одни считают 3.7 Flash избыточным на фоне более дешёвых и быстрых альтернатив, другие — востребованным для быстрых задач, где превосходит Sonnet 5 и Opus.

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

Databricks привлекает раунд Series K при оценке >$100 млрд.
Компания, предоставляющая платформу для аналитики и ИИ, подтвердила переговоры о новом финансировании. Сумма сделки и имена инвесторов пока не раскрываются, но источники называют ориентир выше $100 млрд. Это почти вдвое превышает оценку в $62 млрд, полученную в сентябре 2023 года.

По данным Bloomberg, Databricks выручила за последние 12 месяцев $2,4 млрд, рост 50 % г/г. Компания планирует выйти на IPO в 2025 году.

• Databricks объявил о раунде Series K на $10 млрд при оценке $100 млрд, вызвав волну скепсиса: многие считают это попыткой отложить IPO и избежать реальной оценки.
• Участники обсуждения подчеркивают, что компания за 15 лет и $10+ млрд всё ещё не прибыльна, а продукт (Spark, «обёртки» над Postgres, Lakehouse) кажется переоценённым и дорогим.
• Пользователи жалуются на высокие расходы, долгий запуск задач и сбои в сервисе; конкуренты вроде Snowflake выглядят дешевле.
• Раунд воспринимается как способ «разогнать» оценку и дать ликвидности ранним инвесторам, а не как финансирование роста.
• Сравнения с WeWork, Palantir и OpenAI подчеркивают, что длинные цепочки раундов уже не редкость, но вызывают опасения по поводу «пузыря ИИ».