Category: it

Category was added automatically. Read all entries about "it".

ДР Цертуса 2011

(no subject)

Настоящим объявляю, что все мои персональные данные, тексты, фотографии, рисунки, переписка и т.п. являются объектами моего авторского права (согласно Бернской Конвенции), и оповещаю «ЖЖ» (LiveJournal, Inc / SUP Media) о том, что разглашение, копирование, распространение моей личной информации в коммерческих целях равно как и любые другие противоправные действия по отношению к моему профилю в социальной сети строго запрещены.

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

Гёттинген
17 января 2015 г.
Александр Куклев
ДР Цертуса 2011

Языки программирования

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

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

Для меня язык программирования это, разумеется, инструмент концептуализации и моделирования той или иной предметной области. В первую очередь математических построений, потому что любая другая предметная область пользуется математическими конструкциями (попробуйте сформулировать какую-нибудь бизнес-логику, не прибегая к понятиям пары, списка и числа). Естественно sine qua non для языка программирования в моей голове — возможность записывать на нём концептуально чисто и элегантно известные уже 2300 лет геометрические построения и алгоритм Эвклида.

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

Именно поэтому я столько лет не понимал, когда знакомые математики отмахивались от HoTT со словами “ну, наверное программистам это полезно, но зачем это нужно в математике пока непонятно”. Как это может быть непонятно? Математика кишмя кишит построениями, от и до. Определение какиех-нибудь когомологий это описание того, как их строить. Теорема о неявной функции — это декларативное описание того, как строить функцию по её уравнению.

Мы можем конечно делать вид, что словесное описание с картинками (коим пользовался и Эвклид ещё ~2300 лет назад), это и есть идеальный способ описания построений. Но если бы это было так, не было бы затруднений несколькими умелыми штрихами превращать словесные описания в формализованные машинно-читаемые. Раз это далеко не так, значит в словесных описаниях лишь видимость conceputal clarity, а на самом деле что-то существенное замели под ковёр. Значит должно быть интересно, что именно замели под ковёр, и как этого избежать не теряя в элегантности описания построений. И тут природа как обычно даёт нам подсказку, что мы копаем в нужном месте — тем удивительным фактом, что на пути формализации построений откуда ни возьмись вдруг возникает нетривиальная современная математика.
ДР Цертуса 2011

Hemifields (освежая в памяти...)

Напомню, что для поле (тело) можно эквивалентно определить как (коммутативное) кольцо, где
1) Для всякого x ≠ 0 существует x⁻¹ такое, что x⁻¹x = xx⁻¹ = 1;
2) Для всякого x ≠ 1 существует x*, такое что x* = 1 + xx* = 1 + x*x.

Дело в том, что можно определить x* через (1 - x)⁻¹, а x⁻¹ через x = 1 - x*⁻¹. Для полуколец в зависимости от того, что выбрать, получатся неэквивалентные результаты, т.к. там нет операции «-».

Если выбрать вариант (1), получатся широко известные полуполя, такие как полуполе неотрицательных рациональных чисел или тропическое полуполе. Они превосходно поддаются классификации: на самом деле, все полуполя либо являются полями, либо являются обобщениями указанных двух примеров — тропическими алгебрами частично-упорядоченных групп, либо неотрицательными частями частично-упорядоченных полей и их факторполуполями, см. https://arxiv.org/pdf/1709.06923.pdf.

Если выбрать вариант (2), получаются штуковина, устоявшегося названия которой я не нашёл, назовём пока гемиполями (hemifield) и гемителами. Сюда, разумеется, входят все поля/тела. Но кроме того гемителами являются по определению все полукольца со звездой (star semirings, см. http://stedolan.net/research/semirings.pdf), например полукольцо регулярных выражений, где сложение это |, умножение конкатенация, единица пустая строка, а звёздочка “нуль или более раз”. Канонические примеры гемиполей — гемиполя индуктивных типов данных с точностью до изоморфизма. Сложение это Either[X, Y], умножение Pair[X, Y], звёздочка — List[T]. Для индуктивных типов данных верно, что вообще всякое невырожденное уравнение X = Polynome[X] имеет решение. Это утверждение для обычных полей означало бы алгебраическую замкнутость.

Мне много-много лет интересна задача классификации алгебраически-замкнутых (в указанном выше смысле) гемиполей.

* * *

Напомню, что локальными кольцами называются кольца, у которых для всякого x существует по меньшей мере либо x*, либо x⁻¹. Попробуем назвать локальными полукольцами такие полукольца, у которых для всякого x существует по меньшей мере либо x*, либо x⁻¹. Это общее обобщение полутел и гемител. Имеют ли какие-то хорошие свойства локальные полукольца, являются ли они в каком-то смысле естественными? Имеют ли они какое-то отношение к локализациям, как в случае колец? Существует ли для них какой-то вариант теоремы о том, что все проективные модули (бисемимодули?) над ними обладают базисом?
ДР Цертуса 2011

“Услышь меня, машина” – через 22 года

Как-то зимой 1997-1998 года я зачитался журналом Компьютерра — декабрьским выпуском, посвященным распознованию речи. Особенно меня впечатлила статья Вячеслава Алексеева “Услышь меня, машина” (https://old.computerra.ru/193754/), где рассказывалось, что оказывается можно при помощи датчиков да элеткродиков распознавать внутреннюю речь человека, внутренний монолог. Вот он, убивца кливиатур, подумал тогда я!

Ну в самом деле, когда мы печатаем, мы ведь всегда “про себя” произносим, что печатаем. А тут можно то же самое, только без необходимости тыкать по кнопкам, и, главное, годами тренероваться тыкать по кнопкам с приличной скоростью. Процитирую кусочек статьи полностью: «Появлялись в печати и сообщения о работах по озвучиванию "внутренней речи". На лицевые и другие артикулирующие мышцы испытуемого прикреплялись датчики электрической активности, подключенные к компьютеру. Испытуемый произносил тестовые звуки и слова, а компьютер снимал показания датчиков и строил базу данных образцов, то есть "обучался". Впоследствии, благодаря накопленным данным, программа могла печатать или синтезировать произносимые вслух слова.

Самое поразительное заключается в том, что если увеличить чувствительность датчиков, то они давали аналогичные сигналы и при речи “про себя”. Оказалось, что если думать словами, то на артикулирующие мышцы тоже поступают слабые сигналы возбуждения, аналогичные речевым. Конечно, "подслушать" удавалось только мысли в форме "внутренней речи", составляющей, как выяснилось, далеко не полную картину мышления. Да и то, по отзывам разработчиков, наблюдалась дикая мешанина из обрывков фраз.»

С тех пор (на самом деле, в самое недавнее время) распознание речи скакнуло вмерёд очень качественно, и вот уже я сам надиковываю списки покупок своему смартфону, а он переводит их в текст, так чтобы удобно было пользоваться в магазине. Но аппарата с электродиком всё не появлялось. Что-то мелькало в новостях науки, но потом пропадало. Я как-то выяснил, что первые исследования и первые устройства были задолго до 1997 года (надо поискать, я писал об это много лет назад в ЖЖ), но устройства были громоздки и непрактичны для повседневного использования. А сегодня в ленте попался вот такой прототипчик:
https://www.cnet.com/videos/mit-prototype-can-sense-words-youre-about-to-say/

Страница проекта: https://www.media.mit.edu/projects/alterego/, “AlterEgo is a non-invasive, wearable, peripheral neural interface that allows humans to converse in natural language with machines, artificial intelligence assistants, services, and other people without any voice—without opening their mouth, and without externally observable movements—simply by articulating words internally. The feedback to the user is given through audio, via bone conduction, without disrupting the user's usual auditory perception, and making the interface closed-loop.”
ДР Цертуса 2011

The future is now

Ну что, Lexar показал таки SD-карточку на 1TB и ещё в октябре microSD на 512GB. Естественный вопрос — куда всё это девать*. Но µLED и µOLED на низком старте/на марше, поэтому голографические телевизоры не за горами, а там как раз такие объёмы хранить и понадобится.

А ещё в конце сентября nVidia выпустила архитектуру “видеокарт”, с выделенными подпроцессорами для рейтрейсинга. Утверждается, что впервые в истории на массовых устройствах станет возможен real time ray-tracing — хотя, конечно, не для замены традиционного рендеринга, а для его уточнения с целью получения фотореалистичных деталей (теней, отражений, прозрачных и светящихся материалов, пламени, рассеяния на дыме, облаках, волосах, коже).

_____
* Ну, конечно, понятно, что природная лень программистов и естественное желание их начальства не тратить на оптимизацию ресурсы, которые можно потратить на более быстрый выход продукта на рынок, приведут к тому, что программы и веб-сайты станут жрать совершенно бессмысленно ещё раз в десять больше места. Но я не о том.
ДР Цертуса 2011

Exact arithmetics: Integers and Reals (and “48 bits should be enough” ☺)

Вот почитаешь «Software disenchantment» Тонского, и сразу хочется вернуться к дизайну компьютерных архитектур времён суперкомпьютеров CDC 3000 Сеймура Крэя или Лебедевскомого БЭСМ-6, где в самом деле считали сколько чего нужно, а не разбрасывались ресурсами попусту.

Вот например для кодирования указателей, целых чисел и чисел с плавающей запятой стандартной точности там использовалось по 48 бит, очень приятная длина машинного слова. Было понятно, что 32 бита — это слишком мало, а 64 бита — избыточно для большинства применений.

Я вообще большой поклонник машинной арифметика с fallback'ами, без overflow/underflow. То есть, если результат какого-то вычисления не влезает в машинное слово, в то место, куда надо положить результат, вписывается 0b10...0 (со значением “не влезло на полях, смотрите в сносках”), а настоящее вычисление производится при помощи библиотеки арифметики произвольной точности (“bignum”) и записывается в специальную “таблицу сносок” в отдельном месте памяти, в виде записи “по адресу 0x348973794893 не влезло число, вот оно: 12164510 0408832000”. Ну и соответственно, всё это работает прозрачно: если запустилась какая-то машинная арифметическая операция, а операнд оказался 0b10...0, то вместо машинной операции запускается fallback из bignum-библиотеки, и так далее. При таком подходе понятно как оценивать, какая нужна длина машинного слова: нужно, чтобы на практике необходимость вызывать fallback'и была очень, очень редка, потому что они работают в тысячи и тысячи раз медленнее, чем встроенные операции. Но с другой стороны, каждый лишний бит в машинном слове означает, что встроенная арифметика будет медленнее, транспорт из памяти будет медленнее и в кеши (каждого уровня) будет влезать меньше полезного, чем могло бы. Исходя из этих соображений 48 — очень хороший компромисс.

Кроме того, это хороший компромисс и для чисел с плавающей запятой. 24, 48 и 96 битов для чисел с правой запятой — это гораздо более адекватные стандарты для low-precision real, standard-precision real и high-precision real, чем 16, 32 и 64.

Кстати, в этой области есть интересные недавние подвижки. На смену стандартным IEEE-754 floats предложили новую систему Posit, которая
(а) отказывается от всех этих +0, -1, бесконечностей и NaNов в пользу единственного зарезирвированного значения (на побитовом уровне, кстати, кодируемого тем же самым 0b10...0), которое сигнализирует, что результат операции не является вещественным числом, а чем он конкретно является нужно трактовать по контексту; а в случае когда происходит операция с непонятным результатом, предлагается чтобы случался трап (recoverable exception) и программист сам решал, чего там делать.
(b) использует побитовое кодирование, которое позволяет сравнивать вещественные числа при помощи обычных целочисленных операций сравнения
(c) более разумно распределяет представимые числа по вещественному лучу (плотнее вокруг 1 и 0 и без аномалии с subnormals), что приводит к немножко меньшей потере точности на типовых арифметических операциях и очень хорошей дискретизации сигмоидных функций,
(d) система очень дружественна к операции FUSED ACCUMULATE-MULTIPLY — это такая операция с использованием промежуточного “регистра” большого размера, позволяющая вычислять точное (т.е. без промежуточных округлений) произведение матриц. Это операция является краеугольным камнем всех вычислений высокой точности на числах с плавающей запятой.

Автор системы Джон Густафсон прежде экспериментировал с очень неортодоксальными системами представления чисел с плавающей запятой, но потом внял суровой критике Вэлвла Кагана (основного разработчика IEEE-754, 85-летнего корифея и мастадонта в этой области), и придумал достаточно скромно отклоняющуюся от IEEE-754 систему Posit. Отсутствие всяких NaN'ов с бесконечностями имеет недостатки для SIMD-вычислений, где “ignore and calculate as if it works” (т.е. графика в компьютерных играх), но если требуется предсказуемость вычислений (все остальные случаи), то подход Posit лучше — либо пусть программист заранее проставит флаги, что делать если случилось какое-нибудь деление на ноль или корень из отрицательного, либо пусть ловит эксепшн и решает проблему по-существу.

В интервальной арифметике на позитах “особое значение” в качестве левой границы интерпретируется как -∞, а правой — как +∞. Поэтому в интервальной арифметики восстанавливаются все ценные фичи IEEE-754 (в т.ч. algebraic integrity) и даже больше. IEEE-754«+∞» = (MAX_POS_VALUE, 0b10...0), IEEE-754«-∞» = (0b10...0, MIN_NEG_VALUE), IEEE-754«+0» = (0, MIN_POS_VALUE), IEEE-754«-0» = (MAX_NEG_VALUE, 0).

Надеюсь, когда-нибудь мы доживём и до того, что компьютеры будут на уровне железа поддерживать хорошую интервальную арифметику, чтобы можно было прогнать числомолотилку и получить “обоснованную догадку” (именно это, кстати, и значит слово «posit»), а жесткую вилку, в пределах которой обязан быть результат. Густафсон в общем именно этим сейчас и занимается, насколько я понимаю. Он известен тем, что предложил подход к интервальной арифметике, базирующийся не на замкнутых конечных интервалах, а на связных подмножествах проективной вещественной прямой ℝ̂, получилось очень элегантно — даже корифей и мастадонт интервальной арифметики Ульрих Кулиш (по забавному стечению обстоятельств тоже 85-летний) был крайне впечатлён и отметил, что стандарт интервальной арифметики IEEE-1788, который Кулиш несколько лет разрабатывал с ещё несколькими десятками специалистов, благодаря работам Густафсона устарел ещё до принятия.

В ближайшие годы несомненно будут доделаны языки программирования, поддерживающие точную вещественную арифметику (я к этому имею прямое отношение) в том смысле, что на них можно будет задавать манипуляции над вещественными числами произвольной сложности таким образом, что сколь угодно малая погрешность на выходе будет теоретически достижима, если обеспечить достаточно малую погрешность на входе (что для вычислений ab inito выполнено автоматически) и достаточное количество вычислительных ресурсов (а вот с этим будет проблема). Несомненно также и то, что применительно к инженерным задачам (от моделирования балки до симуляции плазмы) вычресурсов для применения точной арифметики не будет хватать на порядки, и смысл записи решения в терминах вещественной арифметики тут будет не в том, чтобы “запустить и оно посчитало само”, но в том, чтобы иметь работающий потенциально эталон (и слишком тяжеловесный для регулярного практического использования), на который неточным вычислительным алгоритмам можно равняться. Равняться можно в том смысле, что “один разок можно по-честному прогнать на суперкомпьютере за 2-3 месяца” и посмотреть, насколько точный результат отличается от приблизительного, который вычисляется за 2-3 секунды. Но гораздо более важна возможность равняться в смысле возможности писать математические доказательства того, что приблизительные алгоритмы сходятся, стабильны, гарантируют с такой-то вероятностью погрешность в таких-то пределах, и т.д. И для этого нам нужно кроме точных вычислений иметь формальную модель вычислений приближенных, соответствующую фактической модели, реализованной в процессоре. И в качестве таковой интервальные вычисления, капсулирующие проблематику промежуточных округлений, подходят гораздо больше, чем просто вычисления с плавающей запятой по IEEE-754, где эффект округлений хоть и сбалансирован, но абсолютно непредсказуем. Для интервальных вычислений про некоторые алгоритмы можно доказать строгие гарантии — точный результат отличается от приближенного, не более чем на столько-то. Про IEEE-754 такого шанса нет вообще, там любые гарантии могут быть только статистическими.
ДР Цертуса 2011

Грамматики

Я много лет подробно не интересовался вопросами формальных грамматик. С тех пор как появился Perl6 и библиотеки парсерных комбинаторов для Хаскела и Агды, писать парсеры для формальных языков (даже такой сложности как, собственно, Agda) стало удобно, и я как-то перестал интересоваться формальной стороной дела.

Однако же, там за последние годы многое произошло. Меня всегда интересовали естественные обобщения контекстно-свободных грамматик. Контекстно-свободные грамматики являются крайне элегантным формализмом, потому что сочетают в себе как генеративный, так и аналитический подход. Но они, увы, слишком слабы и для естественных и для формальных языков. Для формальных языков нужны “расширимые контекстно-свободные грамматики” (они позволяют работать с ситуациями, когда пользователь определяет в ходе программы новые переменные и операторы, причём если с по части переменных возможен хак, укладывающий их в рамки контекстно-свободных грамматик, то с операторами так уже не выйдет). И про прорывы на этом поприще я пока не слышал, пока с этим действительно удобнее всего работать при помощи парсерных комбинаторов. Тут мне интересна возможность красивого математического формализма и возможность создания эффективных парсеров. Для контекстно-свободных языков-то с парсерами всё с недавних пор совершенно прекрасно. Около 2010-2011 года был разработан парсер Marpa (сильно усовершенствованный парсер Earley 60ых годов), который умеет за линейное время разбирать языки широчайшего класс однозначных грамматик (в том числе, включающий все LL(*) и LR(*)), а всё остальное парсить не хуже чем за n^3. Причём Marpa отлично совместим с ad Hoc расширениями, что позволяет делать отличный хендлинг грамматических ошибок (писать разумные сообщения об ошибках и выдавать очень разумные предложения о том, что пользователь, возможно, имел в виду) и парсить отдельные расширимо-контекстносвободные штуки типа XML. Очень хотелось бы иметь красивый формализм для таких расширимых штук и иметь парсер, который сможет производить разбор за квазилинейное время. Ещё вот недавно для парсеров такого типа придумали штуку под названием Local Lexing (https://arxiv.org/abs/1702.03277), которая позволяет описывать цельно языки с кастомными литералами внутри и элегантно встраивать error handling прямо в спецификацию языка.

Что нужно естественных языков мне, разумеется, непонятно, т.к. я не эксперт, но известно, что в рамки контекстно-свободных языков естественные языки не лезут вообще. Мне всегда казалось, что формализм Tree-adjoining grammars крайне элегантен — это как контекстно-свободные языки, где единицей манипулирования являются не строки, но грамматические деревья. Таким образом можно определить более общий класс языков, чем при помощи контекстно-свободных грамматик, но при этом сохраняются возможности эффективного разбора и понимаемость как в геренативных, так и в аналитических терминах. Но ещё с конца 1980ых известно, что есть синтаксические языковые феномены, которые не укладываются в рамки этого подхода. Пять классических случаев — особенности порядка слов в глагольно-наречных группах в немецком и корейском языках и в именных группах в турецком, наложение падежей в старогрузинском, а также числительные в китайском. Ну и ещё грамматические системы из мира лексикографов, Head-driven phrase structure grammars в эту систему как-то плохо укладывались.

И вот недавно придумали формализм Tree Wrapping Grammar (и лингвистическую парадигму Role and Reference Grammar, обобщающую Head-driven phrase structure grammars и реализуемую грамматическим формализмом Tree Wrapping Grammars). Это красивый слабо-контекстно-зависимый (mildly context-sensitive) формализм, который умеет все эти корейские, немецкие и турецкие извращения.
Видимо, нужно теперь делать эффективные парсеры Affix Tree Wrapping Grammars, сопряженные с Deep Learning AI (для разрешения неоднозначностей).

Поправка: Пока является открытым вопросом, умеет ли TWG _все_ нужные корейские, немецкие и турецкие извращения. k-TWG для конечного k не умеет.

P. S. А вот когда проверяют состоятельность "больших" грамматик для целых языков на корпусах литературы этих языков, как там обращаются с эрративами, диалектизмами, сленгом и сокращениями, которых уймы в художественной литературе и разговорной письменной речи?
ДР Цертуса 2011

Фазовка и искусственный интеллект

Общеизвестно, что при изготовлении мультфильмов вручную вначале рисуется только по несколько кадров в секунду (а то и меньше) — ключевые кадры. Этот процесс называется раскадровкой. Потом (и это, очень часто выполняют анимационные аналоги “литературных негров” — менее маститые художники, иногда даже на аутсорсе в какой-нибудь дешёвой местности) прорисовываются промежуточные кадры. Этот процесс называется фазовкой.

Я был в ранней юности испорчен Autodesk Animator и Macromedia Flash 4.0, где существуют всякие Motion Tweens, позволяющие полуавтоматически интерполировать между ключевыми кадрами. Уже лет пятнадцать tweening (= inbetweening = фазовка) профессионального качества по достаточному набору хинтов доступен даже в бесплатном софте, см. https://en.wikipedia.org/wiki/Synfig
Я думал, во всей анимационной индустрии уже давно только так.

Но недавно мне открыли глаза и рассказали, что в аниме по сей день фазовкой занимаются исключительно живые люди (в основном на аутсорсе в какой-нибудь Корее). Ежели создатели аниме не хотят сразу всё рисовать на компьютере и проставлять хинты, это можно понять. Без хинтов при полной мултипликации, конечно без какого-то количества прорисованных вручную промежуточных кадров не обойтись. Но если рисуется не космический боевик, где всё непрерывно летает и взрывается, то в 99% секундных блоков достаточно нарисовать 5-10 кадров, и остальное может быть интерполировано алгоритмически с идеальным качеством, более детальная ручная фазовка может быть нужна только если делается какая-нибудь очень динамичная и сложная сцена с кучей очень быстро или очень сложно движущихся объектов.

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

Ну, думаю, вот в области автоматического video enhancement такие могучие прорывы в последнее время, и ИИ c deep learning'ами шагают по планете, это же какое-то позорище, то всё это не может нарисовать даже промежуточные 12 кадров, если остальные 12 (т.е. более чем достаточно!) уже нарисованы, и различия между соседними кадрами вообще минимальны.

Погуглил и обнаружил, что в июне 2017 как раз вышла статья об успешном применении ИИ для этих целей: https://arxiv.org/abs/1706.03497.
Видимо, не долго позорищу осталось позорить.

P. S. Вообще, мои представления об условности и штамповости (в т.ч. некоторой картонности) картинки в аниме совершенно перевернулись, после того как я увидел динамические пейзажи (льющийся над озером в парке дождь и т.д.) в работах Макото Синкая. В принципе кое-что можно оценить и по одной картинке:

the-garden-of-words-takao-and-yukino

(советую кликнуть и взглянуть в высоком разрешении).

Я никогда не осуждал аниме за штамповость (причём, чуждую мне штамповость) картинки, подозревая, что использование визуальных штампов — это как раз изрядная составляющая содержательного искусства аниме, важнейшее выразительное средство, в точности как в немом кино: прикладной символизм. Но моему глазу куда приятнее смотреть на наполненную живыми деталями картинку, из-за чего аниме и не привлекало особенно моего внимания (исключая, пожалуй Хаяо Миядзаки, у которого тоже скорее стилизованный реализм).
ДР Цертуса 2011

F* и Agda/Coq

На днях я рассказывал о тяготах программирования сложных вещей на Агде: дела в самом деле обстоят так, что я, не смотря на более чем 10-15 (смотря как считать) лет опыта в машинной верификации и валидации, периодически чувствую себя слишком тупым, чтобы на этом писать:
Проблема в том, что придумать конструкции, корректные по построению. А упираешься в то, что заведомо верно работающий код никак не хочет, например, проходить фазу проверки на отсутствие бесконечного зацикливания, и нет никаких подсказок, почему не хочет. Или есть, но сообщения об ошибках написаны недоступным для человеческого понимания образом. И нужно отгадать и переформулировать. Так, чтобы бездушная машина врубилась.

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

Так вот, на самом деле я считаю, что нет. Я считаю, что для нужд “реального программирования” (исключая местами написание инфраструктурных библиотек) почти всегда удобнее использовать не корректность по построению, а корректность, проверяемую пост-фактум, причём работу по доказательству корректности (или поиску контрпримера) должен насколько это только возможно, перенимать “искусственный интеллект”.

Для реального программирования с контрактами и машинной проверкой корректности на данный момент лучшим является F* (https://www.fstar-lang.org/tutorial/):
– берётся нормальный императивный языка программирования с очень сильной поддержкой функциональщины и ООП (или, если угодно, нормальный функциональный язык с очень сильной поддержкой императивщины и капсюляции изменяемого состояния),
– к нему прикручивается мощная система типов с инструментарием для ограничения побочных эффектов у процедур и контрактов: требований и гарантий для процедур, инвариантов для структур данных и объектов с изменяемым состоянием, локальных и глобальных гарантий для взаимодействующих систем, и
– мощный солвер (в данном случае мощнейший SAT-Solver Z3), который берёт на себя работу по автоматическому доказательству всего, что доказывается тривиально.

Почему же тогда я занимаюсь вещами в ключе Agda, а не в ключе F*? Дело в том, что для того чтобы при помощи F* можно было сделать всё, что хочется делать, сперва нужен достаточно развитый _язык_ для описания тех самых контрактов, требований и гарантий, а также для определения сложнейших с вычислительной точки зрения типов данных, таких как вещественные числа неограниченной точности, взаимодействующие распределённые системы и внешние объекты (в смысле линейных типов).

Создание/доведение достаточного для всех практических и математических задач логического исчисления и языка/proof assistant'а на базе такой теории. Это первый шаг к созданию такого (аналога) F*, на котором будет удобно писать всевозможный софт, для которого есть потребность в верификации и валидации, в т.ч. ядра операционных систем, стеки сетевых протоколов, компиляторы, криптографию, распределённые системы и числодробилки, а также любые библиотеки, фреймворки, сервисы и платформы, предназначенные для широкого использования.
К счастью, второй и третий шаг на этом пути уже сделали создатели F*: они подали пример, как к достаточно приземлённому языку приделать контракты произвольной сложности, и как прикрутить к этому ”искусственный интеллект”, справляющийся с автоматическим доказательством тривиальных вещей в довольно широком разнообразии случаев.
Следующим шагом, по видимому, будет прикручивание ко всему этому ещё и солверов на базе нейронных сеток, которые будут справляться с нетривиальными, но укладывающимися в рамки распространённых подходов случаями. Успехи Machine Learning в последние годы позволяют надеяться, что эта задача будет для них посильна.
ДР Цертуса 2011

Литобзор

Во-первых хочу посоветовать блестящую публикацию Нады Амин и Росса Тейта «Java and Scala's Type Systems are Unsound: The Existential Crisis of Null Pointers» (15–45 минут чтения).

Статья очень хорошо и доступно написана. Разобраться сможет любой, кто прилично знает Java или Scala. Прочитать её будет крайне полезно всем, кто хочет поглубже понять generics в типизированных объектно-ориентированных языках, и не только семейства Java.

Дело в том, что системы типов Java и Scala несостоятельны: авторы приводят код метода `coerce<T>(v)`, который без использования unsafe cast или ещё каких-либо хаков берёт любое значение `v` какого угодно типа и выплёвывает его под видом значения типа `T`. Проблема вскрывается только во время выполнения, при попытке сделать что-нибудь с этим значением.

Идея в том, что алгоритмы проверки типов полагаются на существование объектов определённых типов как на признак заменимости типов (subtyping evidence): такие объекты по идее невозможно было бы сконструировать, если бы соответствующее отношение заменимости типов не выполнялось.
Авторы алгоритмов, по-видимому, упустили из виду, что они работают не с тотальными языками вроде Agda или Idris. В иных языках “пустые по идее” типы можно “населить” незавершающимися вычислениями ⊥ или даже вообще имеется “универсальное значение” null, подходящее в качестве значения любого непримитивномого типа.
Первое не является проблемой для Java, т.к. язык не поддерживает ленивых вычислений, и метод, содержащий расходящееся вычисление, просто никогда не завершится, но для других нетотальных языков надо помнить: в качестве признаков можно использовать только значения, помеченные как неленивые, т.е. подлежащие обязательному вычислению, даже если вычисленное значение дальше никак не используется.