Sanskrit: Язык для верифицированных научных вычислений¶
Общее описание¶
Современные языки для научных вычислений — Python, Julia, R, Wolfram — хорошо решают свою задачу на уровне написания отдельных скриптов, проведения вычислительных экспериментов и т.д. Однако при росте объëма кода на первый план выходят проблемы, связанные с плохой интеграцией библиотек, логическими ошибками и т.д., которые решаются правильно разработанной системой типов. Кроме этого, достаточно сильная система типов позволит прямо в коде доказывать корректность написанных алгоритмов, чего нет ни в одном из перечисленных выше языков и, потенциально, будет являться незаменимым фундаментом для будущих исследований.
С нашей точки зрения, в идеальном языке для верифицированных научных вычислений должны быть средства для решения следующих задач:
- представление табличных данных, матриц и тензоров
- кэширование результатов
- написание собственных (эффективных) алгоритмов
- возможность переиспользования написанных алгоритмов в как можно большем числе различных контекстов
- верификация написанных алгоритмов (и, возможно, доказательство оценок на эффективность, а также на точность приближённых решений)
- ...ваши предложения...
В прошлом году была начата работа над компилятором, языковым сервером и пакетным менеджером языка. Также был предложен дизайн системы типов, основанный на ObsTT (вариант системы типов с зависимыми типами, где тип равенства значений вычисляется по-разному в зависимости от типов значений).
В этом году для выбора доступны следующие задачи:
Поддержка параллельного рантайма в Sanskrit¶
На данный момент, единственным доступным таргетом компиляции для Sanskrit является трансляция в код на C. Предлагается в качестве альтернативного таргета добавить поддержку HVM и сравнить производительность.
Вывод типов на основе унификации в Sanskrit¶
На данный момент, проверка типов в пользовательском коде на Sanskrit производится с помощью классического двустороннего вывода типов. Предлагается добавить в пользовательский код возможности для неявной передачи аргументов, что включает в себя реализацию более сложных и интересных алгоритмов вывода типов.
Архитектура компилятора Sanskrit, основанная на запросах¶
На данный момент, компилятор Sanskrit работает в "классическом" режиме: получает все исходные файлы, проходит все фазы компиляции и возвращает скомпилированный бинарный файл. Однако данный режим работы плохо подходит для эффективной поддержки языка в средах разработки; для хорошей интеграции с языковым сервером, компилятор тоже требуется превратить в своего рода сервер, отвечающий на запросы обновления кодовой базы её инкрементальной перекомпиляцией.
Грамотное программирование на Sanskrit¶
В силу предназначенности Sanskrit для научных вычислений, естественно ожидать, что у него есть режим для literate programming (например, как Jupyter Notebook для Python).
В данный момент такого режима для Sanskrit нет; предлагается его реализовать.
См. также: Код как вики.
Распределённые вычисления на Sanskrit с помощью zkSNARK¶
zkSNARK — одно из новейших изобретений криптографической науки. С их помощью можно:
- доказать обладание некоторой секретной информацией без её раскрытия;
- производить гомоморфные вычисления за разумное время;
- доказывать правильность вычислений, произведённых сторонним агентом, за сублинейное время.
Подобная технология открывает огромное количество возможностей. Например, на её основе можно создать распределённую (динамическую?) систему коллаборативных вычислений, где будет гарантироваться корректность вычислений вне зависимости от намерений участников сети. Звучит прекрасно, осталось разработать дизайн и реализовать.
См. также: Проект по zkSNARK.