https://github.com/aviaryan/awesome-no-login-web-apps

An "awesome list" of Web apps that work without login. Can you believe that?! 😁

The winter is coming. У кошек началась игра пристулов.

For a junior programmer, a programming language is something like Angular or Blockchain, while for a senior developer, a language is Ruby or Python.

Hillel хорош! 😁
https://www.hillelwayne.com/post/sudoku/

https://www.youtube.com/watch?v=PI-eyMVBqqc
Latent Effects for Reusable Language Components

https://arxiv.org/abs/2108.11155

Latent effects are (claimed to be) more modular than Algebraic Effects and Handlers and Scoped Effects. The resulting approach (the data type) looks like heavily parameterised Free Monad. But that provides a way to "construct" (Domain-Specific) languages from completely independent pieces of syntax and semantics (taken from libraries).

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

https://www.cantorsparadise.com/the-web-of-mathematics-a-data-visualisation-baa5d478d908

The Web of Mathematics — an interactive diagram of relations between mathematical fields and application areas.

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

Вызывает смешанные чувства... С одной стороны, видно уважение и желание воссоздать стилистику и тон оригинального материала, с другой стороны — полностью игнорируется трагизм и подтекст оригинала. При этом prodution выглядит дёшево. 😞

Ну и мне хореография и постановка боёв что-то не нравится, хотя показали мало, может, на самом деле выглядит лучше, чем в трейлере.

https://persons.iis.nsk.su/en/pssv21
Program Semantics, Specification and Verification: Theory and Applications

Англоязычная (нынче онлайн-) конференция, организуемая русскими исследователями из Иннополиса и Новосибирска.
Fun fact: на второй день некто Yegor Bugayenko будет рассказывать про EOLANG and φ-calculus. Хочу на это посмотреть.

Oldie but goodie: https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.53.2065
Pure Type Systems Formalized (1993)
by James Mckinna , Robert Pollack

This paper is about our hobby. For us, machine-checked mathematics is a passion, and constructive type theory (in the broadest sense) is the way to this objective. Efficient and correct type-checking programs are necessary, so a formal theory of type systems leading to verified type synthesis algorithms is a natural goal. For over a year the second author has been developing a machine-checked presentation of the elementary meta-theory of Pure Type Systems (PTS) [Bar91], (formerly called Generalized Type Systems (GTS)). This project was blocked until the first author collaborated with a fresh idea. Here we describe the state of this ongoing project, presenting a completely formal, machine checked development of this basic meta-theory, including the underlying language of (explicitly typed) lambda calculus.

Кабы не было ковид в городах и сёлах
Никогда б не знали мы этих дней весёлых

(c) жена

Дельный пост, особенно для начинающих датасаентистов.

I’m not the first to point out that box plots always make distributions look ‘bell shaped’

😏

https://nightingaledvs.com/ive-stopped-using-box-plots-should-you/ — думаю, можно запостить

Испёк блин размерности нуль -- состоит из дырок чуть менее, чем полностью.

https://www.kickstarter.com/projects/958692255/prometheus-wept-a-post-digital-turn-based-rpg

Выглядит интересно. Напоминает про Shadowrun, но мрачнее и жёстче. Почти соло-проект, инди до мозга костей. Но разработчик умеет get shit done, респект.

https://arxiv.org/abs/1505.03118
When causation does not imply correlation: robust violations of the Faithfulness axiom

We demonstrate that the Faithfulness property that is assumed in much causal analysis is robustly violated for a large class of systems of a type that occurs throughout the life and social sciences: control systems. These systems exhibit correlations indistinguishable from zero between variables that are strongly causally connected, and can show very high correlations between variables that have no direct causal connection, only a connection via causal links between uncorrelated variables. Their patterns of correlation are robust, in that they remain unchanged when their parameters are varied. The violation of Faithfulness is fundamental to what a control system does: hold some variable constant despite the disturbing influences on it. No method of causal analysis that requires Faithfulness is applicable to such systems.

Блин, логично. Но контринтуитивно. Вообще засада, а статья ещё 15го года.

https://www.tudelft.nl/en/dhpc

Can you guess the name? No? Then watch the video. 😊

Я давно прикупил. Чего и остальным советую. 😊

Если вдруг кто-то до сих пор не прикупил себе Haskell in Depth, то самое время: сегодня дают скидку 42% на https://www.manning.com/dotd. С той же скидкой можно заодно купить ещё три книжки: для начинающих изучать Haskell от Уила Курта (она отличная, я работал над ней в оригинале как technical proofer, и редактировал перевод на русский), для интересующихся дизайном приложений в функциональном стиле от Саши Гранина, ну и для интересующихся функциональным стилем вообще и не брезгующих при этом синтаксисом Scala от Michał Płachta.

Жир на животе -- это груз прожратых лет.

https://arxiv.org/pdf/2104.13117.pdf
A Verified Decision Procedure for Orders in Isabelle/HOL

Статья безусловно крутая по нескольким причинам, но меня особо повеселило, что она на 200% эксплуатирует "класический Programming Language Theory" подход "для решения любой проблемы нужно просто сделать подходящий язык и систему типов". 😁

Итак, что же делается в статье? Упрощённо, следующее:

1. Кодируется алгоритм (decision procedure) для определения (не)консистентности системы (не)равенств (без кванторов).

1.1. Для представления неравенств, естественно, определяется язык формул с (не)равенствами.

2. Чтобы вообще поставить вопрос о верификации алгоритма, необходимо определить интерпретацию формул. Естественным образом в качестве модели используется функция валюации переменных и рефлексивное, транзитивное, антисимметричное (замкнутое) отношение.

2.1. После чего определяется отношение интерпретации между моделью и формулой.

3. Далее задаётся "абстрактная спецификация" алгоритма (который decision procedure), т.е. записывается логическая формула, которая показывает, когда система (не)равенств противоречива.

3.1. Эта формула записывается в терминах "синтаксической модели", т.е. по факту — ещё одного языка для записи отношений (в данном случае — тупо в виде множества пар, как обычно в теории множеств, но тут — на уровне синтаксиса).

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

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

5. Далее начинается ещё более интересное. Поскольку этот алгоритм поиска противоречий (aka decision procedure) должен использоваться в системе доказательства теорем Isabelle/HOL, верить ему "на слово" нельзя (тогда ошибка в алгоритме приведёт к появлению ложных доказательств), нужно чтобы он сам возвращал доказательство наличия противоречия, которое можно будет проверить на правильность.

5.1. А это значит что?! Правильно, нам нужен язык для записи пруф-термов! И система правил вывода для него.

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

5.2. Тут пришло время ещё одного обобщения. До сих пор рассматривались только нестрогие неравенства (типа ≤), в то время как нужно доказывать и для строгих (типа <).

5.3. Оказывается, проблему можно решить, расширив язык формул операциями конъюнкции, дизъюнкции и отрицания!

5.4. А для нового языка нужна новая (расширенная) система правил вывода с новыми пруф-термами.

5.5. И ещё одна — для доказательства корректности преобразования между формулами.

6. В конце-концов можно всё-таки написать реализацию алгоритма поиска противоречия и доказать его корректность по отношению к спецификации.

7. И после написания некоторого количества интеграционного кода, подрубить эту реализацию к самой Isabelle/HOL.

7.1. Само собой, этот код включает ещё пару промежуточных языков, пару преобразований между ними и систему правил вывода.

Сколько языков и систем вывода было использовано в процессе — посчитайте сами, у меня что-то пальцы закончились. 😁

Не знаю, что за "синтез доказательств", но с остальным согласен! 😃