Верификация частными случаями
Буду говорить в контексте программирования, но соображения можно распространить шире.
Когда мы описываем алгоритм: программу, доказательство теоремы или решение математической задачи — мы строим его описание в рамках некоторой формальной модели. В рамках соглашений и ограничений, которые мы явно или неявно принимаем.
Описать алгоритм вне формальной модели невозможно. Хотя бы потому, что любой язык — уже формализация.
Отсюда вытекает интересная проблема.
Тарантога: второй блин
Потоки данных во второй версии прототипа Тарантоги.
Продолжаю эксперименты. Как видно из заголовка, вторая попытка тоже не удалась, хотя выглядит симпатичнее.
Реализация ушла довольно далеко от описанного в посте о первом блине. В частности, GraphQL не подошёл.
Как всегда, работа породила сторонние результаты. Я подумал об уменьшении сложности работы с данными, вынес в отдельную библиотеку логику работы с предикатами.
Вторую версию концепции я считаю жизнеспособной, но сильно затратной для развития в одного разработчика. Вот если бы меня было несколько, или проект уже существовал в рабочем виде, и надо было только дописывать новых агентов.
Но мы имеем, что имеем, поэтому буду думать дальше. Скорее всего попробую сделать в лоб: минималистично, стандартными подходами без интеллектуальных извращений. Всё-таки представление об инструменте уже несколько раз в голове перекрутил и оно значительно упростилось.
А пока расскажу что получилось на этот раз.
Концепт-документ игры Сказания
](https://tiendil.org/static/posts/concept-document-for-the-game-tales/images/concept-document-for-the-game-tales-cover.png)
Источник изображения: MTG Fetch Lands: What Are They and How to Get Them for Chea
Ещё один концепт, на этот раз довольно старый. Не думаю, что такую игру будет просто привести к успеху, но идея мне нравится.
Python 3 Types in the Wild
Вышла статья с исследованием состояния статической типизации в Python. Я её наискосок просмотрел, всё примерно так, как я и рассказывал в эссе:
Далее несколько интересных цитат.
Бесконечность схем данных
 (с) [Врубель](https://ru.wikipedia.org/wiki/Врубель,_Михаил_Александрович)](https://tiendil.org/static/posts/infinity-of-data-schemas/images/infinity-of-data-schemas-cover.jpg)
Программист думает о путях, которыми ходят байты. Демон сидящий (с) Врубель
Расскажу об одной боли при разработке и проектировании ПО — преобразованиях данных между их схемами. Буду говорить о серверах, как наиболее наглядном и знакомом мне примере, но соображения можно распространить на весь софт.
Для демонстрационных целей местами может случиться некоторое преувеличение.
Рассмотрим простейший проект, этакий минимальный набор:
- один тип клиентов;
- один сервис;
- одно хранилище.
Данные, соответственно, ходят в обе стороны:
- между клиентом и сервисом;
- между сервисом и хранилищем.
Сколько схем данных вы тут видите?