-- У тебя в какой области PhD?
-- TPL.
-- Может, PLT?
-- Нет.

Exciting (promising or provocative) upcoming talks from SPLASH'21:

https://conf.researchr.org/details/aplas-2021/aplas-2021-keynote-talks/1/-Solidifying-and-Advancing-the-Software-Foundations

https://conf.researchr.org/details/sas-2021/sas-2021-papers/4/Exploiting-Verified-Neural-Networks-via-Floating-Point-Numerical-Error (trollface)

https://conf.researchr.org/details/sle-2021/sle-2021-papers/15/SLE-Keynote-Integrating-Usability-into-Programming-Language-Design (finally something tangible on programming languages ease of use?)

https://conf.researchr.org/details/sle-2021/sle-2021-papers/8/Vision-The-Next-700-Language-Workbenches (will we finally get people actually using Language Workbenches at scale? 😃)

https://conf.researchr.org/details/aplas-2021/aplas-2021-papers/11/A-compilation-method-for-dynamic-typing-in-ML (a Standard ML modernization at last! 😂 Actually the authors talk about native compilation of dynamic types along with static types which is interesting.)

https://conf.researchr.org/details/gpce-2021/gpcegpce+2021+-+20th+international+conference+on+generative+programming%3A+concepts+%26+experiences2021/3/A-Variational-Database-Management-System

https://conf.researchr.org/details/gpce-2021/gpcegpce+2021+-+20th+international+conference+on+generative+programming%3A+concepts+%26+experiences2021/13/On-Stack-Replacement-for-Program-Generators-and-Source-to-Source-Compilers (on-stack replacement as a source-level program transformation... sounds simple! 😂)

https://2021.splashcon.org/details/splash-2021-rebase/4/A-Retrospective-on-the-Design-of-the-Swift-Programming-Language (Swift is already so old they're doing a retrospective on it! 😱)

https://2021.splashcon.org/details/splash-2021-oopsla/6/Efficient-Compilation-of-Algebraic-Effect-Handlers

https://2021.splashcon.org/details/splash-2021-Onward-papers/4/Language-guided-Programming (the promise of natural language programming never gets old 😏)

https://2021.splashcon.org/details/splash-2021-Onward-Essays/2/Programming-as-Architecture-Design-and-Urban-Planning

https://2021.splashcon.org/details/splash-2021-splash-keynotes/1/Integrated-Scientific-Modeling-and-Lab-Automation (I suspect Cardelli will tell the same story as before but it's so fascinating! 😃)

https://2021.splashcon.org/details/splash-2021-oopsla/30/Gradually-Structured-Data

https://2021.splashcon.org/details/splash-2021-oopsla/27/Well-Typed-Programs-Can-Go-Wrong-A-Study-of-Typing-Related-Bugs-in-JVM-Compilers (trollface)

https://2021.splashcon.org/details/splash-2021-oopsla/59/How-Statically-Typed-Functional-Programmers-Write-Code (I was one of the subjects so it's interesting what they infer 😃)

https://2021.splashcon.org/details/agere-2021-papers/3/Session-Types-in-Elixir (Exactly what Elixir programmers were missing! 😁)

https://2021.splashcon.org/details/rebls-2021-papers/1/ShapeRank-Rank-Polymorphism-meets-Reactive-Streams (APL punks not dead!)

https://2021.splashcon.org/details/vmil-2021-papers/6/Reflections-on-a-decade-of-MoarVM-a-runtime-for-the-Raku-programming-language (Ever heard of Raku? Perl 6 maybe? And they're doing some interesting stuff...)

https://2021.splashcon.org/details/hatra-2021-papers/10/User-driven-design-and-evaluation-of-Liquid-Types-in-Java (Do Java users need Liquid Types? Indeed... 😁)

https://2021.splashcon.org/details/splash-2021-recent-sigplan/22/Reasoning-about-the-Garden-of-Forking-Paths (We'll finally be able to reason about computational complexity of lazy programs. In Coq! 😈)

https://2021.splashcon.org/details/splash-2021-recent-sigplan/71/Python-3-Types-in-the-Wild-A-Tale-of-Two-Type-Systems ("Surprisingly, when developers use static types, the code rarely type-checks..." Surprisingly? 🤔)

https://www.youtube.com/watch?v=xiFXDKQ7Syk

Ооо!.. Это офигенная идея! Сделано тоже отлично, до середины казалось, что взаправду. Удивительно много комментариев на русском... 😂

-- Нельзя доставать шило из жопы! Это структурный элемент. Без него голова в трусы упадёт.

https://www.cl.cam.ac.uk/~pes20/cpp/popl085ap-sewell.pdf
Mathematizing C++ Concurrency

По слухам, это первая работа по формализации C/C++ Memory Model. Делалась ещё до того как выпустили стандарт 11го года, и более того, финальный стандарт подправили на основе косячков, выявленных в этой статье.

При этом, авторы не только формализовали, но и "механизировали" модель в Isabelle/HOL и доказали корректность предлагаемой компиляции для x86-TSO модели памяти. Но и на этом они не остановились, а сделали ещё и отдельную тулу для проверки C++ программ на отсутствие гонок по данным (и ещё некоторых UB за компанию) — при помощи Netpik, экстракции из Isabelle/HOL, чёрта, беса и доработки напильником, как я сильно подозреваю.

Правда, как я мельком глянул, в стандарте C++20 переписали чуть не половину модели памяти, так что эта формализация уже устарела и представляет исторический или образовательный интерес. Образовательный в том смысле, что она постепенно вводит понятия для описания семантики многопоточных программ на слабых моделях памяти, но тема настолько сложная, что всё равно чёрт ногу сломит, а читать полный Isabelle/HOL исходник вообще страшно...

http://wallcamera.csail.mit.edu/

"Пещера Платона" для нейронных сетей! 😂

https://distill.pub/2021/distill-hiatus/

Управлять журналом тяжело, а инновационным — вдвойне. Или даже на порядок... 😞

Каустическая гитара. 😳

https://github.com/hng/tech-coops

A list of worker-owned tech companies (coops). Seriously cool stuff!
Though no coops from "former USSR" and neighbours...

Кошки думают, что они как в фильме "Fast and Furious", но со стороны больше похоже на фильм "Тупой и ещё тупее"...

https://www.youtube.com/watch?v=sNmOrHw-77U

This was quite, really quite! 😃 There were some sloppy moment, but there are some nice inventive moments. 😊

Thursday 7.10 at 18:30 Matthieu Sozeau is giving an online talk on MetaCoq: https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html. Should be interesting 😊

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

Мой первый вопрос к трём крайним картинам Вильнёва: "в чём смысл, брат?" Режиссёр очень творчески подходит к визуальной составляющей своих картин, он, безусловно, визионер, но, к моему сожалению, очень быстро теряет связь с реальностью и какой-либо логикой происходящего. Например, сцена подъёма космического корабля из воды (на Каладане) — эпична и завораживающа. НО. Какой смысл "парковать" космический корабль под водой???

Ну и продолжая про космические корабли, на Арракисе приземлились они — по видимому — посреди пустыни: никакой погрузочно-разгрузочной и транспортной инфраструктуры, никаких доков, ничего. И это поле Лето адресовал как "космопорт" и распоряжался защищать. Что там защищать-то? 😂

Кстати, про защиту и нападение. Кажется, упрекать современные блокбастеры в отсутствии хоть какой-то военной стратегии и тактики уже даже немного неловко... Не буду заикаться про совершенно бестолковый штурм замка, но прославленные сардуукары даже со штурмом полузаброшенной не охраняемой климатической станции не справились! Для начала они красиво спустились с вершины башни на своих антигравитационных устройствах — прямо в центр засады фрименов, которые по сути ничего и не охраняли, а просто пили кофе в этом месте! 😂 В концовке эпизода выяснилось, что атакующие не догадались взять несчастное сооружение в кольцо (допустим, ни у кого не было плана станции чтобы заранее выяснить все входы и выходы), благодаря чему упустили почти все свои HVT. 🤦‍♀️

Но зато постановка самих сражений на очень высоком уровне. В силу (необъяснённого в фильме, хотя из книги-то мы знаем, в чём дело!) повального использования ножей для уничтожения личного состава противника и сложившейся в Голливуде традиции, основой рукопашного боя в фильме послужила Кали (или Силат, в общем филлипино-индонезийские БИ). Динамично, зрелищно, разнообразно. Не Doug Marcaida против Ray Dionaldo (https://www.youtube.com/watch?v=FQ1WQmvjri0), конечно, и даже не "Рейд", и не "Джон Уик", ну так и жанр не тот. 😃

Отдельно хотел похвалить подбор актёров — мне очень понравился. Единственный минус — Ребекка Фергюсон местами переигрывает, так что Джессика получилась слегка истеричной, даром что Бене Гессерит. 😁 Но, как говорится, "bad acting is bad directing" — как так вышло, что Джессика впадает в истерику, когда Пола "допрашивает" Преподобная, но режет глотки похитителям, не моргнув глазом? Что-то тут слегка не сходится, дорогой Дени. 😏

Ну и я не припомню, чтобы Робан Дейва Батисты хоть с кем-то подрался — остался в недоумении, жду продолжения! 😂

В остальном — отлично, замечательное попадание в образы. Некоторые сцены поставлены особенно тщательно. Больше всего мне запомнилась неудачная попытка отравить Владимира Харконена со стороны умирающего Лето. По-моему, сцена решена даже лучше, интереснее и логичнее, чем в книге.

Так что, немало есть в новой "Дюне" на что посмотреть — местами поулыбаться — надеюсь, насобирают в прокате на следующую! 😁

PS. Ещё забыл смешной момент: в фильме все всегда снимают маску или платок с лица ровно перед облаком пыли. Ну и очки вообще не носят — песок же в глаза никогда не попадает. 😂

https://docs.google.com/document/d/e/2PACX-1vSt2VB1zQAJ6JDMaIA9PlmEgBxz2K5Tx6w2JqJNeYCy0gU4aoubdTxlENSKNSrQ2TXqPWcuwtXe6PlO/pub

Инженеры из команды Chrome попытались выразить Rust-like ownership and borrowing system на шаблонах C++. Понятно, что ничего не вышло, но они подробно описали в каких местах сломалось и почему.

https://drewdevault.com/2021/09/23/Nitter-and-other-internet-reclamation-projects.html

"Internet reclamation" -- "человеческое лицо" для "корпоративного Интернета". 😄

Надо тоже автоматические редиректы настроить -- Твиттер и Ютуб чем дальше, тем больше разламываются. 😒

Такого ещё не видел! 😅

Слышали, что ещё придумали эти зумеры? Микродозинг образования! 😂
https://ru.wikipedia.org/wiki/%D0%9C%D0%B8%D0%BA%D1%80%D0%BE%D0%BE%D0%B1%D1%83%D1%87%D0%B5%D0%BD%D0%B8%D0%B5

я считал, что механизм логического вывода на правилах - это явная альтернатива ML там, где нет возможности собрать достойный датасет

Вот так зумеры смотрят на эту вашу формальную логику! 😁

Рубрика "угадай язык программирования".

The return value of a subroutine is "OK", "bad", or "very bad"

Никаких других вариантов возвращаемых значений в языке нет вообще! 😂
(Ответ: FurryScript)

Аааа!!! Алан Кей сидит онлайн на Quora прямо сейчас и отвечает на мои комментарии!!! 😱

Это что-то фееричное и невероятно милое: https://play.fancade.com/ 😃