Update 29 Dec 2025: https://thedeemon.dreamwidth.org/

Ссылки на избранные посты, чего тут было интересного.

Про язык ATS и зависимые типы:
https://thedeemon.livejournal.com/41035.html - можно начать тут
https://thedeemon.livejournal.com/tag/ats и дальше набор постов по тэгу. 2011

Про Clean и уникальные типы. 2011

Об информации. 2011
"... выведем некоторые важные факты теории информации и напишем на чистом функциональном языке компрессор, который будет сжимать лучше, чем zip, rar, bzip2 и 7z в их дефолтных режимах. Потом оглядимся вокруг, в том числе на физику, и в результате, надеюсь, что-то поймем об информации."

свобода, равенство, унивалентность! - про гомотопическую теорию типов. 2013

Я вижу квантовые операторы - 3D визуализация волновых функций и операторов с объяснениями и онлайн демкой. 2016

Общая теория относительности: время, черные дыры. 2015
https://thedeemon.livejournal.com/97291.html
https://thedeemon.livejournal.com/97778.html

В искривленном пространстве: визуализация неевклидовых пространств изнутри. 2018
https://thedeemon.livejournal.com/127151.html
https://thedeemon.livejournal.com/127473.html
https://thedeemon.livejournal.com/127697.html

Пишем неправильный компилятор. 2010
https://thedeemon.livejournal.com/9712.html - серия постов начинается тут.
https://thedeemon.livejournal.com/tag/leo - и другие посты про него же.

Категорические вычисления (язык CPL) 2012
и продолжение/дополнения раз два три.

Про Йонеду и про должения 2012

Колдунство реификации 2013
"Только сегодня в нашем бродячем цирке великий йог и аскет Лямбдагарбха продемонстрирует уникальный фокус материализации! Имея полиморфную функцию, оперирующую произвольными типами (полифорфными, не конкретными), функциями из них и туплами, только зная ее тип и умея ее вызывать, он материализует ее исходник, даже если она скомпилирована в другом городе..."

Про язык Dafny 2015

Про корейский язык 2021

Про китайский язык 2021

IDFPC: соревнование по программированию, что я организовал в 2012 году. Участникам понравилось. Если не подглядывать, задачки оттуда и сейчас может быть интересно порешать.

Про фрактальное сжатие изображений 2012

Наслушавшись похвал в адрес оконного менеджера Niri, пару недель назад решился его поставить, консультируясь у ИИ по всем возникающим вопросам. Эта штука управляет окнами, по умолчанию растягивая их по вертикали на весь экран, а по горизонтали - на сколько-то (у меня по умолчанию 50%, с возможнстью переключиться на 100% или 1/3 или 2/3), и при создании новых окон старые не меняют размера, а все выстраиваются в горизонтальный ряд, который обычно шире экрана, и по нему можно скроллить. И таких горизонтальных рядов можно иметь сколько угодно, перемещаясь так в 2D по виртуальному пространству из окон. Управление с клавиатуры очень простое, быстро привыкаешь.

Первое впечатление сразу после установки самое яркое, конечно: серый экран и только памятка про горячие клавиши, которыми можно управлять окошками (но ни одного окна еще не создано), и пара кнопок чтобы запустить шелл alacritty (который у меня не был установлен) и какой-то лончер, которого у меня тоже не было. В итоге ничего запустить вообще было нельзя, только выйти вон можно. Но ничего, поставил какой-то лончер wofi (список программ с поиском для запуска оных), настроил запуск нужного шелла (Warp сначала не хотел работать, но заработал после установки xwayland-satellite), и для всяких удобств и красот я поставил шелл Noctalia, рисующий наверху бар со всякой информацией и менюшками управления тем и сем, и он же за обои отвечает. Получилось весьма приятно:



Еще поначалу оказалось, что не могу на русский переключиться. Оказалось, включается изменением одной строки в файле настроек Niri. Причем закомментированный образец там как раз про русскую раскладку. Потому что автор Niri - некий Иван Молодецких, похоже с моего факультета в МГУ, и участвующий в той же лаборатории машграфики, где я сам был 20 лет назад.

В редакторе Zed, как и в терминале, настроил немножко прозрачности, мне нравится как зелень с фона слегка проступает, так оно приятнее чем на однородную стену пялиться. Так и живу теперь, очень доволен.



Кстати про Zed. Оформил подписку, чтобы разные AI агенты через него использовать. Он там в биллинге показывает, сколько каких токенов потрачено, и порой довольно неожиданные цифры получаются. Например, вот был у меня с GPT-5.2 один диалог, где он работал с одним единственным исходным файлом парсера на 25KB (~3600 "слов" согласно wc), он там не с первого раза нужный результат получил, итерации три ушло, в сумме несколько строк поменялись. При этом контекст был заполнен на 100к токенов, а в биллинге возникли 250к Input Tokens и аж 1.3 миллиона Input Cache Read Tokens. Откуда? Такое ощущение, что он там еще по интернету ходит читает всякую документацию и код, пока над задачей думает. Или это что-то другое, кто знает что за кэш там?



А еще там однажды Gemini ***нулся на отличненько, впав в бесконечный цикл. Весело.

Интересно, кто сможет это увидеть.

У меня кириллические сервисы выключены, соцкапитал низкий, потому возможно побуду тут в некириллической части, плюс вот тут есть копия журнала: https://thedeemon.dreamwidth.org Там будет и продолжение. С Новым Годом!

Из относительно недавних находок и новых привычек, заметно улучшивших ежедневный опыт использования шелла. Программка zoxide добавляет в шелл однобуквенную команду z, заменяющую cd, она запоминает посещаемые папки, и потом в них можно перемещаться, указав только название самой папки, а не выписывать полный абсолютный или относительный путь. Когда есть несколько проектов или мест, где что-то делаешь, потом пишешь просто "z foo" или "z bar" где бы ты ни был, и тебя понимают с полуслова, целиком путь к ним помнить не нужно. А с учетом автодополнения в zsh чаще получается просто "z f<RIGHT ARROW><ENTER>" или "z b<RIGHT ARROW><ENTER>", даже и имя проекта целиком писать не надо. Супер удобно. И да, "z -" возвращает в предыдущую локацию, а "z" - домой.

А, и в рифму, чтоб два раза не вставать. Оказывается, в редактор Zed завезли Helix mode, и в последней версии им уже можно пользоваться. Я раньше для разных проектов использовал то vscode, то Helix. Один хорош для навигации и поиска по большому проекту, второй хорош для непосредственно работы с исходным текстом. Когда-то давно смотрел на Zed, и тогда он был еще молод и проигрывал по обоим применениям. А сейчас развился, оброс темами и расширениями, vim mode и helix mode, и стал объединять в себе хорошие стороны и vscode и Helix. Пусть не идеально, но уже кажется юзабельно. Плюс там есть поддержка ИИ помощников от разных поставщиков - claude, grok, chatgpt, gemini... Я раньше их почти не использовал, в том числе потому что в Helix'e их не было и не ожидается. А тут есть все и сразу. В общем, пробую теперь Zed в качестве основного редактора, посмотрю что получится из этого.

Заметил, что уже два года использую компьютер не так, как делал это предыдущие лет 30. А именно, стал использовать auto tiling, когда окна на экране не заслоняют друг друга, а автоматически делят меж собой все пространство экрана. Несколько (переменное количество) виртуальных экранов, меж которыми легко переключаться с клавиатуры. На каждом экране если одно окно - оно занимает его целиком. Если два - делят пополам. Три - 0.5/0.25/0.25, Четыре - опять поровну, и так далее, хотя на практике никакого далее не случается, больше 3-4 окон на одном экране не держу. Ближе к углу экрана, в системной шапке, показана карта рабочих столов и окон на них, например, такая:



Когда к такому режиму привыкаешь (а это довольно быстро происходит), то потом самое интересное случается, когда вдруг оказываешься на системе с традиционными окошками произвольных размеров. Обнаруживаешь, как много ментальных усилий / времени / энергии уходит там на то, чтобы окошки ресайзить, двигать, переключаться. Раньше этого не замечал, а теперь замечаешь. И понимаешь, насколько жизнь проще, когда этого самому делать больше не надо.

Среди нердов-линуксоидов популярны tiling window managers, коих сейчас целая куча (i3, bspwm, sway, awesomewm, xmonad, hyprland, mangowc и пр.), но они обычно выглядят страшно и требуют массу времени на настройку и освоение. У меня же прижился вариант попроще - обычный GNOME (который мне нравится как выглядит) с расширением Forge, которое и делает автотайлинг. Как обычно в tiling WMs, активное окно выделяется цветной рамкой, перемещать фокус между окнами на экране, менять их местами и пр. можно с клавиатуры простыми сочетаниями клавиш, а можно мышкой. В какой-то момент поставил себе его в качестве эксперимента, да вот уже два года так и живу, и на что-то другое менять пока не собираюсь.

Про Gullstrand–Painlevé coordinates - систему координат с интересными свойствами для описания решения Шварцшильда для простой статичной черной дыры - я слышал давно. Но только на днях узнал, что Painlevé ее открыл, будучи в промежутке между двумя своими сроками на посту премьер-министра Франции. "Эх, мы о таких премьерах можем только мечтать!" - говорят английские профессора Brian Cox и Jeff Forshaw в своей книжке Black Holes.

Интересный момент в корейском языке: там есть чудесный глагол, означающий "дела обстоят таким образом", в инфинитиве это 그렇다 (кырота) - "to be so", "to be that way", где первый слог 그 (кы) значит "вот то", "that".

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

그래서 (кыресо) - “So / therefore” - "поэтому / следовательно"
그러니까 (кыроника) - “So / that’s why / I mean” - "из-за этого"
그러면 (кыромён) - “Then / in that case” - "если так"
그리고 (кыриго) - “And / and then” - "и / и потом / а также"
그러나 (кырона), 그렇지만 (кырочиман) - “However / but / still” - "однако / тем не менее"
그런데 (кырондэ) “But / by the way” - "но / однако"
и просто фразы
그래 (кырэ) или 그래요 (кырэё) - "ок, да, это так". Дословно "дела так обстоят".

(и да, в японском есть прямой аналог: それ "сорэ", где そ "со" тоже значит "that", и там получаются слова それで, それなら, それに, それでも, それだから и др.)

В фильмах и сериалах эти все слова очень часто звучат.
Недавно я досмотрел сериал, который на нетфликсе называется Crash Landing on You (в оригинале 사랑의 불시착 - Love's forced landing). Там первая половина происходит в Северной Корее, а во второй половине несколько северных корейцев оказываются в Южной. И я заметил, что северные корейцы там говорят не так, как южные, даже когда слова все те же самые используют. Первое, что замечаешь, это что во всех этих словах вместо "кырэ" у них звучит "кирэ", и в других местах часто "ы" заменяется на "и". Получается, северные корейцы и́кают. Во всяком случае, в этом сериале.

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

Я очень редко играю в игры, но в этом месяце неожиданно увлекся одной, да так сильно, что потратил там часов 60 пока не дошел до финальных титров. Это Watch Dogs Legion, игра вышла лет 5 назад, и как будто никто о ней ничего хорошего не слышал, вы будете первые. Я помню, несколько лет назал когда услышал какие-то анонсы про нее, подумал "о, это как GTA только в Лондоне, интересно". Потом года 3 назад подписался на сервис игр в облаках GeForce Now, поставил ее там, часик покатался по городу, да забросил. В тот момент как-то не до нее было, и лень было вникать. По сюжету там действие происходит в недалеком будущем в антиутопическом Лондоне, где после серии терактов частная военная компания взялась за обеспечение безопасности, но разумеется переусердствовала, поэтому город заполнен ее солдатами, которые всех обижают, повсюду ее логотипы, дроны, тотальная слежка и т.п. В реальности мы до такого пока не дожили, но если полистать твиттер, то может сложиться ощущение, что уже к тому близко. :) В общем, спустя годы я вдруг решил еще раз попробовать в нее поиграть, и в этот раз сильно протащился.



В первую очередь конечно тем, как здорово там воспроизвели центральную часть Лондона, насколько он узнаваем (ниже скриншотов добавил). Я за годы с начала ковидных времен исходил пешком этот город вдоль и поперек, по крайней мере западную его половину и центр, и радость узнавания реальных улиц и зданий меня в игре ждала на каждом углу практически. Разумеется, почти все самые знаменитые места тут стали вместилищами для миссий, поэтому по мере прохождения побываешь внутри и замка Tower, и моста Tower Bridge, небоскребов The Shard и Walkie Talkie, наведешь шухер в зданиях MI6 и New Scotland Yard, на территории Buckingham Palace и под ней, внутри телевышки BT tower, внутри и под Battersea power station (из которой сейчас торговый центр сделан кстати, в реальности и в игре), внутри башни с Big Ben и т.д. Пара миссий проходят буквально через дорогу от моего офиса. :) Они не стали копировать все улицы один в один, а сжали все, убрав неважные улочки и оставив важные, но в целом география вполне узнаваемая, поэтому ориентироваться довольно легко.

( Read more...Collapse )

Сыну на лето в школе дали список книг почитать, среди них Six Easy Pieces Фейнмана, где он рассказывает про двухщелевой эксперимент с электронами, дескать если их запускать через забор с двумя дырками и ловить на экране дальше, то каждый конкретный электрон попадет в какую-то случайную точку, а распределение этих точек будет выглядеть как результат интерференции волн. Он много говорит "в эксперименте видим то", "в эксперименте видим сё", но перед этим предупреждает, что вообще-то именно в таком виде эксперимент не делали, и описываемый эксперимент только мысленный. Впрочем, говорит, было много других экспериментов, где подобное квантовое поведение наблюдали.

А недавно я услышал в одном подкасте с Jacob Barandes один интересный момент: он говорит, что если мы захотим посчитать, какое именно должно получиться распределение попадания частиц на экране, казалось бы тривиальнейшая задачка в КМ, то мы до сих пор не знаем как это правильно сделать. Казалось бы, вот начальное значение волновой функции, вот мы ее по уравнению Шредингера эволюционируем во времени, и вот она приходит на экран, и мы там можем взять квадрат модуля ВФ и из него получить распределение вероятностей попадания в разные места. Но! Мы же это делаем, взяв значение ВФ в какой-то момент. А в какой? Когда именно электрон прилетит на экран? Этого мы не знаем. В каждый момент времени он потенциально может быть найден где угодно, ВФ нам говорит вероятности его нахождения в разных местах. Если мы зафиксируем момент и произведем "измерение" координаты, получим какую-то точку. А в какой момент это делать? В каждый конкретный момент частица скорее будет где-то еще, а не на экране. Вот простой пример:



Тут яркость обозначает амплитуду волновой функции, а цвет - комплексную фазу. Исходно частица локализована в небольшое круглое облачко (гауссиан) и в комплексной плоскости ее ВФ закручена так, чтобы иметь испульс для движения вправо. По мере эволюции облачко расплывается в пространстве и сначала в целом движется вправо, встречает представленную потенциальным барьером стенку с двумя щелями, частично проходит через них (а большей частью отражается от стенки), там дальше корридор (я добавил сверху и снизу стенки, чтобы отражения интереснее давали картинку) и в конце стоит голубой экран, на котором мы как бы частицу ловим. Справа от экрана я показываю яркостью квадрат модуля ВФ на самом экране в каждый момент, отнормированный. Видно, что в разные моменты там несколько разные картинки. Можем ли мы какую-то одну из них считать предсказанием? Вряд ли. Можем ли как-то суммировать и усреднять? Тоже непонятно, мы не знаем с какими весами суммировать, каково распределение по времени событий прилета частицы. Оператора времени в КМ нет, время - не observable величина. И если в какой-то момент частица прилетает, то ВФ схлопывается, дальше эволюционировать старую ВФ уже нельзя, поэтому как и что тут суммировать - неочевидно.

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

Исходники симуляции, если что, здесь.

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

Из старого поста Сабины Хоссенфельдер на эту тему:

One of the particles gets caught behind the horizon and falls in, the other escapes. The result is a steady emission of particles from the black hole horizon. It’s simple, it’s intuitive, and it’s wrong.

Hawking’s is an illustrative picture, but nothing more than that. In reality – you will not be surprised to hear – the situation is more complicated.
...
This simple image that Hawking provided for the non-specialist is not backed up by the mathematics. It contains an element of the truth, but take it too seriously and it becomes highly misleading.

Скопирую сюда, что недавно писал на одном форуме:

В 1974 году Хокинг выпускает сначала короткую заметку на пару страниц, а затем в 1975 более длинную и подробную статью, где описывает рождение частиц в результате образования черной дыры. Реально описанный им механизм звучит примерно так. Берем простейшее скалярное эрмитово поле и сначала смотрим на него в плоском пространстве, где никакой ЧД еще нет. Его можно разложить через Фурье "по частотам", как сумму простых волн, и исходно в разложении там будут положительные и отрицательные частоты во времени. Частота во времени определяет энергию, частиц с отрицательной энергией не бывает, и при переходе к квантовому полю и операторам, положительным и отрицательным модам соответствуют операторы уничтожения и создания частиц положительной энергии.
Вакуумное состояние по определению не содержит реальных частиц, и значит для каждой моды воздействие оператора уничтожения частицы на него дает ноль.

Дальше у нас образуется черная дыра, пространство искривляется, появляется горизонт событий, и в этой новой геометрии базис, по которому мы раскладываем поля, изменяется, это больше не старые простые волны в плоском пространстве, а новый набор базовых решений, с учетом наличия горизонта событий. Преобразование Боголюбова позволяет перейти от старого базиса к новому, выразить новые базисные моды через линейную комбинацию старых и наоборот. И тут можно заметить, что квантовое состояние, которое было вакуумом в старом базисе, в новом базисе уже вакуумом не является: для каждой моды можно посчитать матожидание количества таких частиц в этом состоянии, и оно выражается через коэффициенты пребразования между старым и новым базисом, и оказывается ненулевым. Т.е. если изначально в плоском пространстве у нас был вакуум, то это самое состояние в новом базисе новой геометрии уже содержит реальные частицы, это больше не вакуум. Эти реальные частицы и есть излучение Хокинга. Ни слова о виртуальных частицах.

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

Тут Хокинг понимает, что это все слишком абстрактно и неинтуитивно, и хорошо бы придумать какую-то операционную картину, что-то более понятное и ощутимое, и выдает в порядке бреда что-то про виртуальные частицы отрицательной энергии, которых вообще вроде как не бывает, но они могут туннелировать через горизонт внутрь ЧД, где время в метрике имеет другой знак, а потому снаружи кажется, что там у них положительная частота и энергия, так эти небывалые частицы своим туннелированием несут снаружи поток негативной энергии. Но добавляет "It should be emphasized that these pictures of the mechanism responsible for the thermal emission and area decrease are heuristic only and should not be taken too literally."

В конце 80-х он выпускает книжку для широкой публики, которую нельзя пугать сложными словами про базисы операторов квантовых полей, и там он выдает еще более примитивную картинку про пары вирт. частиц, еще более далекую от реального механизма из своих работ. Именно эту сказку все запоминают и с тех пор считают описанием излучения Хокинга, хотя и каждый раз удивляются массе несуразностей в ней (что за негативные частицы там и почему именно они падают в ЧД, а не другие).