Самая сильная логическая система, которая только может быть: http://inutile.club/estatis/falso/
Мало кто знает, но уже много лет существует поддержка прямо в Isabelle/HOL и Coq! 😂

https://jupyterbook.org/intro.html

Что-то вроде продвинутого MD-book с возможностью вставки интерактивных Jupyter-backed примеров кода. Может пригодиться для подготовки учебных материалов.

Интересно, почему Slack загружает свой интерфес, а потом всё стирает и загружает его заново? 🤔

https://monto-editor.github.io/about/

Анонсировано как что-то типа ещё более модульного Language Server Protocol для тех, кто хочет написать один раз плагин и использовать во всех редакторах.

https://github.com/svenkeidel/sturdy

A Haskell library for specifying sound and modular abstract interpreters. The authors promise (or even claim having formally proven it) your abstract interpreter will be sound-by-construction because you build it gluing together sound components (with combinators that preserve soundness). Sounds very cool.

Прикольная инфографика. Самое интересное — компании, про которые я бы и не вспомнил. 😅

Java 过于弱智:

https://ethanzuckerman.com/2016/06/22/the-worst-thing-i-read-this-year-and-what-it-taught-me-or-can-we-design-sociotechnical-systems-that-dont-suck/

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

Ну и классическое "да чего там может быть сложного?!" в отношении проблем, про которые мы не имеем ни малейшего понятия. 😊

https://blog.codefrau.net/2021/08/what-is-croquet-anyways.html

Crazy JavaScript (and Wasm in the future?) tech: VMs running in a browser synchronized through a mesh of repeaters. Even end-to-end encrypted for a good measure. Instantly multi-user collaborative persistent apps.

https://esoteric.codes/blog/jon-corbett

Абсолютно другой подход к языку программирования как концепции. Плюс некоторые инсайты в культуру индейцев и её конфликт с нашей культурой.

https://qntm.org/clean

Жёсткая критика книги Clean Code Боба нашего Мартина. 😊
Я-то, конечно же, Clean Code не читал, не испытывая пиитета перед Мартином, но согласен со многими его высказываниями. С другой стороны, с автором заметки я тоже в основном согласен: примеры кода, которые он выдернул из книги — это жесть! 😂
Тем не менее, местами автор явно придирается к Мартину и к его коду. Кроме того, не знаю, что он имеет против SOLID как такового.
В целом, конечно, если кто-то говорит правильные вещи, но сам делает через задницу — это как минимум странный человек. Но я лично если слышу разумные советы — мотаю на ус и стараюсь им следовать вне зависимости от того, следует ли им сам автор.

https://esoteric.codes/blog/bouk-monkey-satirical-code-used-by-people-who-dont-get-the-joke

Кое-что про программистов, язык Go, Open Source и внимание к лицензиям. 😏

-- У тебя в какой области 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...