Paulson's blog is a gift that keeps on giving:

If you think doing mathematics in a modern proof assistant is difficult, let me remark that doing mathematics in a formalised calculus is a bit like using the kind of proof assistant we had 40 years ago.

from https://lawrencecpaulson.github.io/2022/02/23/Hereditarily_Finite.html
😄

https://lawrencecpaulson.github.io/2022/02/09/Ackermann-example.html

I guess I just bound to repost almost every Paulson's post, but this one is insanely cool! More about the Ackerman function than you ever thought there is! 😄

https://blog.burntsushi.net/transducers/

Did you know you can use an FSM as a data structure to implement both Sets and Maps? With fuzzy search and regex search? In a streaming fashion so you don't have to keep all of your data in RAM all the time?

Sounds too good to be true? In this somewhat old post Andrew Gallant describes how to do it with references to papers on FSM representation optimization and actual implementation in Rust. Plus some performance benchmarks.

In the last section Andrew discusses major limitations of the approach and some workarounds to partially mitigate them. Also you'll learn that this technique is employed in production inside Lucene and Elastic Search.

Только что позвонили спамеры из компании "Чёрная бухгалтерия". Я не шучу, так и представились: "компания "Чёрная бухгалтерия". 😳

https://proofassistants.stackexchange.com/a/940/333

This answer is golden, it links to all of the best materials on Type Theory and related subjects.

https://www.forbes.ru/forbes-woman/448097-koding-tol-ko-dla-devusek-zacem-sozdavat-zenskie-obrazovatel-nye-programmy-v-it

Обзорная статья, "на пальцах" рассказывающая про курсы и мероприятия "только для женщин" в сфере ИТ. За подробным обсуждением "не сексизм ли это" и почему, видимо, следует почитать FAQ от тех же Django Girls.

https://obua.com/publications/philosophy-of-abstraction-logic/2/

Abstraction Logic has been introduced in a previous, rather technical article. In this article we take a step back and look at Abstraction Logic from a conceptual point of view. This will make it easier to appreciate the simplicity, elegance, and pragmatism of Abstraction Logic. We will argue that Abstraction Logic is the best logic for serving as a foundation of mathematics.

I found this link somewhere in Paulson's blog. Haven't read but sounds ambitious! 😄

Turns out there's a metric for size increase for mechanized math dubbed "de Bruijn factor": https://www.cs.ru.nl/~freek/factor/

Apparently in practice it's around 4, and in some cases a hair bigger than 1. 🧐

https://mitchellh.com/writing/contributing-to-complex-projects

Some nice guidelines on becoming a contributor to a complex (open source) project.

Не трогал PowerPoint (MS Office в целом) лет 10 или около того. Но тут по случаю решил воспользоваться — думал, за то время что я на него не смотрел, он должен был сильно похорошеть. Но нет, Office от своих традиций не отходит! Вчера вечером сохранил презентацию — сегодня утром PowerPoint не может её открыть, говорит, нужно восстанавливать. Конечно же, восстановить он её тоже не смог — потерял половину слайдов. Самое смешное, что Only Office открыл её почти ровно в том виде, как она была сохранена, несмотря даже на "восстановление". 😂

Nah, Only Office lost all the formulae from all the slides after a couple of save-loads too. 😒

I'm watching an oldish talk by Guy Steele Jr.: https://www.youtube.com/watch?v=ftcIcn8AmSY
At the QnA session he mentions that lessons from the Fortress language somehow informed Julia's evolution... 🤔

And by the way regarding presentations. WPS Office saves the day. Apparently it reads pptx files better than MS Office and has no problems saving them back to disk. Though I've also exported to PDF just to be sure. 😁

Apparently "it's not a bug, it's a feature" can be traced back to 1922 the latest: https://plato.stanford.edu/entries/paradox-skolem/#2

[It] is not a paradox in the sense of an antinomy … it is a novel and unexpected feature of formal systems.

Jean van Heijenoort on Thoralf Skolem's Paradox. 😂

https://arxiv.org/abs/2203.16211
Lay-it-out: Interactive Design of Layout-Sensitive Grammars
Fengmin Zhu, Jiangyi Liu, Fei He

Layout-sensitive grammars have been adopted in many modern programming languages. However, tool support for this kind of grammars still remains limited and immature. In this paper, we present Lay-it-out, an interactive framework for layout-sensitive grammar design. Beginning with a user-defined ambiguous grammar, our framework refines it by synthesizing layout constraints through user interaction. For ease of interaction, a shortest nonempty ambiguous sentence (if exists) is automatically generated by our bounded ambiguity checker via SMT solving. The soundness and completeness of our SMT encoding are mechanized in the Coq proof assistant. Case studies on real grammars, including a full grammar, demonstrate the practicality and scalability of our approach.

It's effin' interactive framework utilizing SMT-solver and proved correct in Coq! Though I don't thing they mean "GUI" when they say "interactive framework".

https://www.actema.xyz/?goal=U29jcmF0ZXM6KCksIEh1bWFuOjooKSwgTW9ydGFsOjooKTsgSHVtYW4oU29jcmF0ZXMpLCBmb3JhbGwgeDooKS4gSHVtYW4oeCkgLT4gTW9ydGFsKHgpIHwtIE1vcnRhbChTb2NyYXRlcyk%3D

Looks like a visual (drag-n-drop) editor for composing (first-order) proofs.

Moving forward with Lawrence Paulson fanboyism finally watched https://www.youtube.com/watch?v=tYqbbRsx8DI (which aired almost a year ago):

... turns out to verify computer systems you need Mathematics, and the more advanced systems you verify the more advanced Mathematics you need.

And other profound observations. "Obvious" statements that authors don't even really bother to mention but require pages to prove 100% rigorously is something even I had encountered.

Also "residual doubt" regarding mechanised proofs from working mathematicians. Though I suspect educational value of legible structured proofs is heavily underappreciated.

https://www.scattered-thoughts.net/writing/the-shape-of-data

Любопытный пост, собирающий в кучку интересные идеи из разных мест. Во-первых, он справедливо разделяет вопрос модели данных и записи (нотации) данных. Во-вторых, между делом вводит 4 уровня моделей данных в языке программирования (на примере Rust):
1. уровень машины
2. уровень "небезопасного" (unsafe) языка
3. уровень "безопасного" языка
4. уровень приложения
(ср. уровни TCP/IP и OSI).
Далее обсуждается связь модели данных и её записи на уровне данных приложения, и что бы мы хотели от обеих для большего удобства разработки.

Актуально для разработчиков новых языков программирования и для преподавателей существующих (чтобы обращать внимание на места расхождения модели и нотации).

https://www.ribbonfarm.com/2022/02/10/tools/

Fundamentally reducing the complexity of tooling required to do a thing requires understanding the thing itself better. Simpler, more user-friendly tooling is the result of improved understanding, not increased concern for human comfort and convenience. You have to get more engineering friendly to generate such improved understandings before you can get more user friendly with what you learn. Complex tooling usually gets worse before it gets better.

If you try to skip advancing knowledge, you end up with tools that try to be more user-friendly by becoming less physics-friendly, and the entire experience degrades.

Also in addition to "user-friendliness — physics-friendliness" dimension the author introduces dimensions of "praxis and poeisis". Yeah, that's weird you should read the piece to get it.

https://www.youtube.com/watch?v=LJ4W1g-6JiY

Пятнадцатиминутка научпопа на нашем канале. В общем, выясняется, что до "бесплатной" энергии ядерного синтеза нам ещё как до Луны пешком. 😒 Мне так кажется, что по уровню развития технологии примерно как для атомных электростанций в 1930х: мы уже строим полномасштабные станции (на этот раз в Китае), но работают они всё ещё в минус.

Текущий рекорд отдачи самого синтеза — 70%. Т.е. пока что сам процесс жрёт больше, чем возвращает чистой энергии. И это без учёта энергии, требующейся чтобы вообще создать условия для синтеза. На экспериментальной китайской международной мегаэлектростанции обещают поднять показатель до 1000%. Да, синтезировать в 10 раз больше энергии, чем закачано. Одна проблемка — в общей сложности для своей работы электростанция будет потреблять на два порядка больше энергии, чем пойдёт на синтез. Ну и как они собираются горячую плазму превращать в электричество и с каким КПД — я не в курсе. Из расчёта с КПД 50% окажется, что станция будет потреблять всего лишь в 2 раза больше, чем отдавать обратно в сеть. Это, безусловно, технологический прорыв, но до экономического и энергетического прорыва всё ещё безумно далеко.

Ну и ссылка на то же самое в виде отзыва на книгу, чтобы вам долго не искать: https://www.nytimes.com/2021/08/19/books/review/the-star-builders-arthur-turrell.html

And now a Math education section: https://www.susanrigetti.com/math

The main contribution of the post is a selection of English textbooks covering general BSc Math curriculum. Thus mostly books on continuous math: Calculus, Linear Algebra, Analysis, intro to Differential Equations. Though nice additions are books on "Introduction to (formal) proofs" which includes such a gem as "How to Solve" It by G. Polya, and a selection of "electives" which includes somewhat impressive (for such a limited format) of texts on Philosophy of Math.

Apart from that I recommend to take notice of How to Study section. But the most interesting part for those of us already out of college (or a university) is "Popular Math Books" — a really solid list with such an eternal classics as "A Mathematician’s Apology" by G.H. Hardy himself! I'd like to add a couple more recent titles:
https://www.amazon.com/Sleight-Mind-Ingenious-Mathematics-Philosophy/dp/0262043467/

https://www.amazon.com/Mathematical-Fallacies-Paradoxes-Dover-Mathematics-ebook/dp/B00A62Y0DU/

https://www.amazon.com/Humble-Pi-Comedy-Maths-Errors/dp/0141989149/

Happy reading and learning! 😁