Гамарджоба.

Курсы (предварительные)

• Семинары по ML

  Этот курс подойдёт для R&D-исследователей из других областей, которым интересно, что происходит, но неинтересно отличать кошечек от собак с помощью fit_predict(), и для настоящих машинлёрнеров, которые чувствуют себя окопавшимися в своей подобласти (CV, например) и хотят узнать, что за туса в других частях. (Подготовить и рассказать свою классную статью очень приветствуется!)

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

  В отличие от других курсов на школе, в которых могут учить делать что-то руками методом лекций и задачек, этот направлен скорее на концептуальное понимание (мы будем читать и может быть выводить формулы, но писать сколь-либо много кода не будем) и горизонтальность (если вы шарите за X – расскажите, у нас семинар).

• Purescript

  PureScript — чисто-функциональный язык, заимствующий многие идеи у Haskell, но предназначенный для компиляции в JavaScript.

  На курсе вы получите:

  • краткое введение в функциональное программирование
  • немного персональной практики
  • коллективное исследование языка — написание нашей собственной реализации Virtual DOM

  Курс будет разбит на две последовательные части:

  • Основы: введение в PureScript и ФП. Чистые функции, эффекты, монады, синтаксис языка.
  • Практика: хакинг VDOM. Посмотрим, что внутри у фреймворка Halogen. Реализация своих diff и patch. Обход деревьев. Взаимодействие PureScript с JavaScript.

  Можно начать с первой, чтобы аккуратно погрузиться, или сразу нырнуть в VDOM.

• Приключения Логических Интегральных Схем

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

  На самом деле CPU и все его варианты — это очень частный случай того, что можно сделать в железе. Для того, чтобы понять, что можно сделать в железе, на него нужно смотреть не в терминах программирования (циклы, вызовы функций и т.д.), а в других, аппаратных терминах: комбинационное облако и элементы состояния, конвейеры и очереди, такты и задержки внутри такта, определяющие тактовую частоту.

  В последние 30 лет проектировщики микросхем не рисуют цифровые схемы мышкой на экране, а синтезируют их кодом на языке описания аппаратуры: Verilog или VHDL. Этот код внешне поход на программы, но имеет другую семантику, которую мы и покажем в этом курсе. Когда код разработан, его можно синтезировать в дизайн физической микросхемы (так делают новые схемы) или превратить в граф из логических элементов и прошить в память FPGA.

  FPGA - это микросхема, на которой соединения транзисторов программируется.

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

  Помимо простых лаб с FPGA мы покажем как строить RISC-V процессор и применять FPGA для обработки звука. Посмотрим на FLOSS-средство проектирования ASIC Open Lane — альтернативу коммерческим пакетам от Synopsys и Cadence.

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

  План курса:

  • День 1. Комбинаторная логика - вычисления без тактов. Языки описания аппаратуры, маршруты ASIC и FPGA, а также жизнь в электронной индустрии.
  • День 2. Последовательностная логика, тактовый сигнал и конечные автоматы. Применение для распознавания музыки.
  • День 3. Две стороны процессора - архитектура и микроархитектура. Разбор минималистичного ядра schoolRISCV.
  • День 4. Против лома нет приема: почему специализированный ASIC на порядки быстрее CPU. Конвейеры, очереди, встроенные блоки памяти и вопросы тактовой частоты. Применения для GPU, сетевых чипов и ускорителей машинного обучения.
  • День 5. Формальная верификация, применение С++ для разработки проектов на FPGA и на десерт: разбор примера с процессором внутри FPGA, подключением к VGA и игрой тетрис.

  Пререквизиты: можно ничего не знать о микроэлектронике, всё расскажем! Нужно уметь программировать и обладать компьютерной грамотностью.

• Zero-knowledge proofs

  ZKP - одна из самых захватывающих и ценных теорий, стоящих за Web3. За последние 4-5 лет количество проектов, использующих ZKP, резко возросло – их можно использовать практически везде: от создания доказательств передачи активов до решения проблем масштабируемости. Это делает ZKP новым фронтиром Web3 и децентрализованных систем.

  Цель этого курса - показать математику, стоящую за ZKP, и предоставить некоторые практические знания. Мы погрузимся в современные фреймворки и DSL ZKP и посмотрим на практические применения.

  Требования: базовые знания абстрактной алгебры (группы, генераторы групп), криптографии (цифровые подписи) и алгоритмов. Знание языка программирования Rust (умение читать и писать код с трейтами Fn*) приветствуется.

• 10 исчислений Isabelle

  Сейчас модно писать про системы доказательства теорем, основанные на зависимых типах. В основном так вышло благодаря усилиям Кевина Баззарда по популяризации Lean Prover среди “чистых” математиков. Это хорошо, но недостаточно хорошо, поскольку обходит вниманием системы, основанные на логике высшего порядка и просто-типизированном λ-исчислении; системы, у которых больше библиотек и индустриальных кейсов.

  В то время как на счету Coq имеется CompCert, на HOL4 верифицировали компилятор CakeML, а на Isabelle/HOL — микро-ядро seL4. Тот же HOL4 использовали для формализации семантики инструкций x86, POWER и ARM. Lean 3 знаменит библиотекой Mathlib, систематически формализующей обширные области современной математики, но по широте охвата она всё ещё уступает Archive of Formal Proofs — каталогу библиотек для Isabelle/HOL, постоянно пополняемому и поддерживаемому в актуальном состоянии.

  Такой перекос в известности тем удивительнее, что теории зависимых типов объективно сложнее логики высшего порядка. Более того, зависимые типы хуже поддаются автоматизации, и такие инструменты как QuickChick и CoqHammer появились через несколько лет после своих аналогов для Isabelle/HOL — Nitpick и Sledgehammer. А язык Isabelle/Isar остаётся образцом для записи структурированных, человекочитаемых доказательств.

  Если вам уже интересна Isabelle/HOL, то половину своей задачи курс выполнил :)

  Вторая половина — тесно познакомиться с инструментами формальной теории языков программирования: исчислениями, их семантикой и метатеоремами.

  Для этого начнём с введения в программирование и доказательство свойств программ в Isabelle/HOL, после чего перейдём к неспешному разбору статьи “A Verified Decision Procedure for Orders in Isabelle/HOL”. Статья постепенно строит и верифицирует всё более и более сложные языки (исчисления) для выражения суждений об отношении порядка между объектами (что-то больше, чем что-то другое, но меньше или равно чему-то третьему). Примеры простые, но не игрушечные — в конечном итоге верифицированная разрешающая процедура для теории порядков была включена в саму Isabelle/HOL, и теперь мы можем её использовать для автоматического получения доказательств.

  Если времени хватит на всё, то мы приобщимся к таким явлениям как реляционная семантика, (доморощенная) система доказательств и её пруф-термы, и уточнение декларативных спецификаций до исполнимых.

  Пререквизиты

  • Базовое функциональное программирование
  • Основы формальной логики

• SAT / SMT

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

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

  Первая задача, которую начали решать солверы, это SAT, то есть задача определения выполнимости булевых формул. По теореме Кука-Левина эта задача является NP-полной и, скорее всего, не имеет полиномиального алгоритма для ее решения. Однако это не так уж плохо: во-первых, существует множество эвристик и алгоритмов, которые ускоряют переборное решение SAT-задачи, а во-вторых, многие теории просто не разрешимы, то есть не существует алгоритма, который мог бы найти решение за конечное время.

  В этом курсе мы:

  1. Изучим основу любого солвера - алгоритмы конфликтно-ориентированного обучения дизъюнктам (CDCL) и Дэвиса-Патнема-Логемана-Лавленда (DPLL). Алгоритм CDCL решает SAT-задачу, а DPLL позволяет легко присоединить к нему разрешающую процедуру, то есть алгоритм, который решает уравнение в определенной теории.
  2. Рассмотрим различные теории (линейную арифметику, битовые векторы, массивы, указатели) и их разрешимость. Если теория не разрешима, то мы постараемся выяснить ограничения, при которых она становится разрешимой, а также изучим соответствующие разрешающие процедуры.
  3. Посмотрим на применения в operations research, криптографии и верификации.

• Современные Лиспы

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

  ФП уже никого не удивить, но с REPL и TDD, чтобы сразу тестировать и видеть результат, его совмещают не так часто. Вся наша практика будет очень интерактивная, программы интроспектируемые в рантайме, и циклы обратной связи суперкороткими.

  Кроме REPLов, Лиспы также известны своей гомоиконичностью и макросами, и в ходе курса мы будем активно метапрограммировать: добавлять новые фичи в язык и делать data-driven eDSL и интерпретаторы к ним. Будем вкладывать одни диалекты Лиспов в другие, запускать один код на разных рантаймах, делать разметку, вёрстку, запросы к БД, манипуляцию данных – всё в одном языке.

  Также мы кратко пройдём по истории семейства Лиспов и посмотрим, какие фичи идеального Лиспа сейчас есть в разных диалектах.

  В конце концов, мы нырнём в скобочный мир с головой: настроим IDE Лиспом, сделаем веб-приложение Лиспом, опишем ОС Лиспом, и задеплоим тоже Лиспом (Elisp, Clojure(Script), Guile Scheme, Guix).

• Статический анализ

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

  Мы возьмем небольшой модельный императивный язык программирования на базе Lua. Далее мы реализуем для него интерпретатор, а после — анализатор потоков данных на примере различных абстрактных доменов. Все это мы будем делать на языке функционального программирования OCaml или его диалекте — Reason. В процессе мы будем изучать всю необходимую теорию, а также обсуждать практические детали реализации, иными словами, как написать код анализатора достаточно лаконично, красиво и расширяемо.

  Темы с точки зрения теории, которые мы разберем:

  • Основные понятия статического анализа
  • Почему идеальный статический анализатор на самом деле создать невозможно, но при этом мы не опускаем руки
  • Синтаксис и семантика программ
  • Абстрактная интерпретация
  • Решетки, алгоритмы поиска неподвижной точки и их эффективность
  • Монотонные фреймворки для анализа потоков данных

  Пререквизиты:

  Чего знать не обязательно:

  • Статический анализ (собственно, зачем, если мы на курсе и будем изучать его основы)
  • Монады, решетки (узнаем) и прочие словечки
  • OCaml / Reason, Haskell и прочие языки семейства ML (научимся)

  Однако, при этом желательно иметь какой-то базовый опыт программирования в функциональном стиле. Как минимум не бояться операций map, filter и fold над списками.