Хорошее введение в Calculus of Constructions

Наверняка многие из вас слышали про языки с зависимыми типами. Кто-то смотрел примеры кода на Agda и Idris2, а кто-то, возможно, даже отложил себе в закладки замечательные книги серии Software Foundations, описывающие тонкости применения Coq (и все никак не может начать их осваивать, да :)).

Авторам канала всегда нравилось разбираться в деталях технологий: территория неизвестного и непонятного манит и требует решительных действий! Как можно пользоваться инструментом, если не понимаешь, как он устроен внутри, хотя бы приблизительно?!

Пытаясь разобраться в особенностях calculus of constructions, мы наткнулись на великолепный документ, описывающий эту теорию типов с самых азов. В тексте даются все необходимые пререквизиты и вводятся базовые обозначения, которые понадобятся для погружения в мир CoC. Этим «Typed Lambda Calculus / Calculus of Constructions» значительно отличается от других подобных работ, требующих от читателя немалого багажа и погруженности в предмет.

Если вы заняты в сфере, где safety — важный quality-атрибут, самое время обратить внимание на мир языков с зависимыми типами. С каждым годом эти инструменты будут все популярнее.

#digest

TigerStyle!

Не знаем, как у вас, но у нас на работе несколько раз рождались серьезные споры о том, какой стиль кодирования следует предпочесть для той или иной кодовой базы. Кто-то спорит до хрипоты, на какой строке оставлять фигурную скобку в коде на C/C++, кто-то обсуждает, использовать ли do-нотацию в Haskell и запиливать ли катаморфизмы, или обойтись простым и прямолинейным кодом свертки.

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

В недавнем выступлении на конференции Systems Distributed CEO компании TigerBeetle, Джоран Грииф (Joran Greef), рассказал про их собственный подход к разработке, названный TigerStyle. Посмотреть выступление можно по ссылке. В текстовом виде TigerStyle описан на GitHub.

Это не совсем Style Guide в привычном нам виде: многие разделы рассматривают довольно серьезные, порой даже философские вопросы, далекие от исключительно проблемы оформления кода.

Делитесь в комментариях вашими любимыми стилями кодирования, а также Style & Design гайдами.

P.S. Удивительно, что весь бизнес TigerBeetle строится вокруг продукта, написанного на языке Zig, который, хоть и на слуху, но довольно редко применяется в крупных проектах. Подходы, принятые в компании, подкупают некоторым пуризмом, например отказом от внешних зависимостей, которые сложно контролировать, особенно в современном мире, где популярны supply chain атаки. Впрочем, это уже совсем другая история :)

#digest

Стековые и «национальные» языки программирования: а что насчет корейского?

Райан Брейнард (Ryan Brainard) описал интересную параллель между языками с обратной польской нотацией и современным корейским языком: они строятся по схожим принципам, ведь предложения имеют структуру субъект-объект-действие.

Райан кратко рассказывает об устройстве стековых языков и далее объясняет, как ту же механику можно применять для корейского.

Наверняка многие задумывались, почему так мало распространены «национальные» языки программирования, ключевые слова в которых записываются понятными носителю словами. Что до авторов канала, то нас подобные языки отпугивали в первую очередь из-за синтаксиса: если в C, Python или Ada заменить ключевые слова на кириллические аналоги, мало что поменяется — код останется более формальной записью сильно упрощенного английского. Однако Брейнард показывает: код на «корейском» языке программирования может оказаться легко читаемым, поскольку будет почти полностью соответствовать реальным предложениям на этом языке!

Вот такое необычное наблюдение. Самсунг, где ваша смекалочка?

#digest

Невербалика и публичные выступления

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

Если личный бренд для вас — не пустой звук, и вы планируете выступать на публике (а возможно уже это делаете), то вы хотя бы раз задумывались, как сделать ваши выступления привлекательнее для зрителя.

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

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

Уилл Стивен (Will Stephen) провел свое выступление, не рассказав ничего полезного. Его доклад — пародия на значимые выступления известных личностей. Но это не просто стендап: через юмор Уилл доносит до зрителя принципы невербального общения со зрителем, которые помогут докладчику притягивать аудиторию.

Доклад Уилла также научит подмечать и избегать типовых штампов, которые часто скрывают недостатки в содержании или подготовке выступающего.

А еще попробуйте выключить звук и посмотреть несколько отрывков. Кажется, что докладчик рассказывает о чем-то очень серьезном и важном, а также полностью разбирается в материале! :)

#digest

Rust to Assembly

Rust продолжает набирать популярность, в него начинают верить крупные компании, все больше проектов пишут на этом языке.

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

Rust to Assembly — серия статей про то, как разные фичи языка компилируются в машинный код. Авторы разбирают разные примеры ассемблерных листингов, полученных после компиляции той или иной конструкции языка, и описывают все нюансы ее низкоуровневой реализации.

Интересная тема, чтобы поковыряться в низах ближайшие пару-тройку вечеров :)

#literature

Реальная безопасность в Linux

Помните время, когда считалось, что Linux — очень безопасная ОС, не то что Windows? Когда казалось, что под Linux нет злонамеренного ПО – например, вирусов – и вообще это оплот безопасности?

К сожалению, это миф, когнитивное искажение, порожденное популярностью Windows. «Винда» просто была популярнее, и потому на нее были обращены взоры всех хакеров мира. Да и в сравнении с закрытой ОС, Linux выглядел более защищенным, ведь на его код смотрели тысячи глаз.

Впрочем, современные ОС далеко шагнули вперед в плане безопасности. В системы добавляли и развивали механизмы, необходимые для изоляции приложений друг от друга и от остальной системы. К примеру, команда, ответственная за безопасность в Google, продумала действительно крутые архитектурные решения для Android, Chromium и ChromeOS, используя в основе ядро Linux. А до этого известная эксперт по информационной безопасности Йоанна Рутковска (Joanna Rutkowska) запустила проект QubesOS. Идея этих архитектурных решений — изоляция приложений в песочницах, для которых можно гибко задавать разрешения на использование системных сервисов и общение с другими такими же приложениями.

Интересно, что в самом ядре и базовых системных сервисах вокруг него уже есть все необходимое, чтобы выстроить достаточно безопасное пользовательское окружение. Тем не менее, популярные дистрибутивы Linux редко используют доступные механизмы контейнеризации, чтобы ограничивать приложения друг от друга и от использования определенных системных вызовов. Все же модель угроз современных GNU/Linux систем недалеко ушла от legacy мира Unix.

Один из членов группы PrivSec опубликовал статью, где разобрал основные проблемы современных дистрибутивов на базе ядра Linux, а также предложил, как каждый из нас может сделать свою систему гораздо безопаснее. Конечно, придется поколдовать!

#digest

Простое введение в завтипы

Почти все слышали про современные функциональные языки программирования со строгими системами типов. Например, про Haskell. Этим языком и темами про монады и монадные трансформеры уже никого не удивить. Зато про языки с зависимыми типами слышали далеко не все, хотя это очень интересная и многообещающая история.

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

Статьи и книги, объясняющие базовые принципы таких языков, к сожалению, часто достаточно объемны, а хотелось бы поверхностно ознакомиться с темой, чтобы понимать, инвестировать ли в нее время.

К счастью, есть неплохая статья 2009 года с введением в зависимые типы на примере языка Agda. В ней авторы демонстрируют несколько примеров того, как языки с завтипами могут статически решать проблемы, которые раньше разрешались только на стадии исполнения.

#literature

nanochess и bootOS

Иногда люди создают программы исключительно ради искусства.

К примеру, проект nanochess не имеет никакой практической пользы, кроме удовольствия от низкоуровневого программирования. Ну и конечно, обучения. В рамках этого проекта был разработан десяток простых игр, написанных на ассемблере для Intel 8088. Каждая из них умещается в один сектор дискеты, 512 байт. А еще автор проекта, Оскар Толедо (Oscar Toledo), опубликовал несколько книг с комментариями к исходному коду игр, объяснив, как они работают.

Позже Оскар создал маленькую дисковую ОС, bootOS, специально для запуска этих миниатюрных игрушек. Она позволяет просматривать простую файловую систему, стартовать из файлов игры и программы, а также вводить их в шестнадцатеричном виде. И конечно же вся эта система также помещается в загрузочный сектор, а максимальная длина любого файла на диске равна 512 байтам :)

#digest

Монадные трансформеры Haskell

В нашем недавнем посте мы вспоминали Haskell с присущими ему концепциями, заимствованными из теории категорий. Вспоминали и монадные трансформеры.

Статей, объясняющих, что же это такое и как этим пользоваться, много. Но найти хорошую и понятную непросто :) Возможно вам понравится одна из свежих, что мы нашли где-то на hacker news.

#literature

Использование model finding при разработке компилятора

Chapel — язык программирования, созданный для упрощения параллельных вычислений.
Компилятор этого языка, Dyno, использует нетривиальную логику для разрешения имен: например для того, чтобы понять, что требуется вызывать — метод с именем foo или одноименную функцию.

В процессе реализации авторы компилятора придумали несколько ухищрений, основанных на битовых картах, которые оптимизируют многократный поиск по пространству имен. Но как показать, что этот подход всегда выдает корректные результаты?

Один из авторов рассказал в своем блоге, как решил использовать известный model finder Alloy 6 для моделирования возможных состояний и поиска контрпримера. Простая модель на Alloy позволила доказать, что исходный алгоритм был неверным, и существовали примеры программ, в которых происходило неверное разрешение имен.

Хороший аргумент за использование формальных методов. Особенно столь легковесных и простых в применении.

#digest

Введение в формальную верификацию программ

Много слышали про использование формальных методов, но не успели погрузиться в эту область? Не знаете с чего начать? Попробуйте ознакомиться с пособием Александра Сергеевича Камкина «Введение в формальные методы верификации программ». Как нам кажется, эта небольшая книга дает достаточно полное введение в столь непростую и интересную область.

С каждым годом спрос на формальные методы в разработке высоконадежного ПО будет расти. И это не только про самолеты и атомные станции: формальные методы широко применяются, например, для верификации смарт-контрактов в blockchain платформах. Дерзайте!

#literature

Избавление от зависимости

Давненько не было у нас внутренних кеков :)

#fun

Введение в системное программирование под Plan 9

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

Возможно, кто-то заинтересуется немного необычной альтернативой подобного курса, которая изложена в бесплатно распространяемой книге «Introduction to Operating Systems Abstractions Using Plan 9 from Bell Labs». Автор книги, Франсиско Бальестерос (Francisco J Ballesteros), рассказывает о типовых системных абстракциях, доступных в Plan 9, и показывает, как ими можно воспользоваться на практике.

#literature

xv6 на Rust

Многие, конечно, уже слышали про xv6 — маленькую операционную систему, разработанную в качестве методического пособия для курса MIT 6.828.

Эта игрушечная, но вполне полноценная Unix-система хорошо описана в этой книге Расса Кокса, Франса Каашоека и Роберта Морриса (Russ Cox, Frans Kaashoek, Robert Morris). На наш взгляд, это издание, дополненное кодом самой ОС, — лучшее введение в архитектуру операционных систем из доступных сегодня.

xv6 всегда привлекала внимание исследователей и хобби-разработчиков благодаря подробному описанию, простой реализации, ортогональному набору возможностей и способности работать на современном железе. Например, авторы xv6 не так давно перенесли ее на RISC-V и решили использовать эту архитектуру в качестве базовой для курса. Так что система адаптируется к «модным трендам» в мире системного программирования.

А что там насчет безопасных языков программирования, например Rust? Ведь RISC-V + Rust было бы мегакомбо, не так ли?! Что же, сразу два проекта на Github занимаются переписыванием xv6 на Rust: octox и rxv6.

Приятного погружения!

#literature

A Tiny Linux-compatible Kernel

Большинство курсов по разработке ОС фокусируются или на ядре Linux, что может быть слишком для непосвященных студентов, или на примитивных учебных ОС, которые совсем далеки по сложности от своих старших собратьев. Кажется, нужно что-то среднее — например, система, достаточно продвинутая, чтобы запускать бинарники из GNU/Linux.

Сказано — сделано, и Владислав Вальчев (Vladislav Valtchev) создал проект Tilck, цель которого — разработать минималистичное ядро ОС, совместимое с Linux на бинарном уровне. Так, чтобы можно было брать программы, собранные для этого популярного ядра, и запускать в учебной ОС.

Пожелаем автору удачи в его проекте, а сами го ковыряться в исходном коде!

#digest

Floppy Bird

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

Что же, вот еще один шедевр низкоуровневого программирования: игра, работающая без операционной системы, Floppy Bird. По названию вы, наверное, уже догадались, что она копирует механику знаменитой Flappy Bird с мобильных устройств. Игра написана на ассемблере x86, и работает в реальном режиме, используя сервисы BIOS.

#fun

Технология аппаратной виртуализации

Гипервизорами с поддержкой Intel VMX или AMD-V уже никого не удивить. Даже если вы не используете в своей работе виртуальные машины, они незаметно присутствуют в вашей повседневной жизни. Например, Windows 10 использует Hyper-V для создания защищённого компартмента, внутри которого исполняются важные для системы функции.

Но как работают расширения виртуализации в вашем процессоре, и просто ли написать свой гипервизор?

Можно обратиться к официальной документации Intel или AMD, погрузиться в исходный код KVM, Xen или ACRN, чтобы разобраться в вопросе досконально. Но можно удовлетворить свой технический интерес и более простым образом, обратившись к хорошему туториалу, где автор уже все разжевал для читателя.

Такой материал мы сегодня и посоветуем: серию уроков по разработке гипервизора для Intel от Ryanfam.

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

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

#digest

Изучаем ассемблер ARMv8 на примерах

Если вы спросите у системного программиста, хорошо знакомого с ARM-платформой, что бы вам почитать, чтобы освоить 64-битный ассемблер ARMv8, то он, вероятно, ответит, что нужно читать ARMARM (ARM Architecture Reference Manual). Это действительно всеобъемлющий документ, позволяющий глубоко познакомиться с платформой.

Но если вас интересует только практическое введение в ассемблер для этой архитектуры, советуем обратиться к статье "A Guide to ARM64 / AArch64 Assembly on Linux with Shellcodes and Cryptography". Это очень удачное и понятное введение, снабженное неплохой практической частью, где авторы реализуют различные криптографические алгоритмы непосредственно на языке ассемблера.

#literature

Наглядная демонстрация алгоритма сжатия JPEG

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

Статья Омара Шехаты (Omar Shehata) на сайте Parametric Press наглядно демонстрирует работу алгоритма сжатия изображений, используемого для формата JPEG.

Каждый этап сжатия изображения наглядно показан в интерактивных демонстрациях-экспериментах, где читатель может настраивать некоторые параметры.

Подобного явно не хватает во многих ВУЗах на занятиях алгоритмами и структурами данных, правда? 😁

#digest

Легковесные формальные методы для верификации примитивов синхронизации

Мало кто не слышал про такие проекты, как seL4 или CompCert, потратившие невероятное количество сил на формальную верификацию микроядра операционной системы и компилятора языка Cи соответственно.

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

Сегодня мы хотели бы поделиться ссылкой на страницу, на которой Расс Кокс (Russ Cox) собрал всю историческую информацию про верификацию примитивов синхронизации в ядре Plan 9.

Применение Spin/Promela помогло найти реальные проблемы в реализации рандеву, что использовалась в системе, ну и, конечно, исправить ее.

Обратите внимание, насколько просты модели на этом языке. При помощи Spin/Promela можно верифицировать сетевые протоколы, примитивы синхронизации и параллельные алгоритмы.

Инструмент за долгие годы существования стал стабильным и быстрым, его отлично документировали. Почему бы не попробовать его в своих задачах?

#lilerature

Макро-RISC-V

RISC-V любят за открытость спецификаций: например, многие ресечеры в академической среде выбирают именно эту архитектуру в качестве основы для своих работ. Даже всем известный учебный проект операционной системы xv6, как мы уже видели, переехал на RISC-V, оставив позади легаси платформы x86.


Вендоры железа не отстают, и уже можно встретить достаточно производительные платы на базе этой архитектуры. Дрю ДеВолт (Drew DeVault) даже пробовал одну из таких железок в качестве десктопа, и оно было почти юзабельно.


Но и хобби-проекты часто выбирают эту открытую архитектуру за основу. Так в рамках проекта Pinapple One Филип Скандера (Filip Szkandera) разработал макропроцессор с архитектурой RV32I на простой дискретной логике. То есть это полноценный 32-битный процессор, правда собранный на нескольких логических микросхемах, и работающий с очень низкой частотой — порядка половины мегагерца.


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


#digest