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! 😁

If anyone is interested Google broke its Meet in Firefox. Good job everybody! 👍

Do you remember you can implement a Turing Machine in Microsoft PowerPoint: https://www.youtube.com/watch?v=uNjxe8ShM-8 ?
Turns out you can also do fractals and some other recursive things: https://www.youtube.com/watch?v=b-Fa6HtvGtQ !
Which is amazing! The only thing about PowerPoint that's more amazing than that is it can't read back the files it saves.

https://www.youtube.com/watch?v=wbJQTtjlM_w
A video of presentation and a discussion between participants of a pretty famous recently project applying Machine Learning to some cutting-edge mathematics.

Here's a Nature article which has a link to an arXiv preprint: https://www.nature.com/articles/d41586-021-03593-1

In addition to the Church of the Least Fixed Point I propose "β-reduction Witnesses".

Serendipitously stumbled upon https://mathematicswithoutapologies.wordpress.com/2015/05/13/univalent-foundations-no-comment/ and it's kinda curious to revisit the answers from 7 years ago.

The most obvious is that Univalent Mathematics indeed grew to dominate research at least in Foundations of Mathematics and Type Theory.

Second, I don't think we can say mechanized proofs are widespread (though that's pretty vague) but I bet the panellists would be surprized how far they penetrated already. And we still have 28 years to go which seems like a lot considering the rate of the spread.

“One doesn’t read a mathematical paper, what one gets is the idea to reconstruct the argument it’s not that people (generally speaking) would be …checking the logic line by line — they would go and extract the fundamental idea; that’s really the essential thing.”

I would say exactly the same about mechanized proofs. For one thing you don't even need to check the proof line-by-line, a machine already did that. Second, I'm huge fan of structured proofs exactly because they show you the shape of the argument and help extracting the major ideas and relationships behind it.

Near the end the author raises concerns of a technological lock-in into a particular system. With the current state of affairs and pretty "heated competition" among different systems that seems unlikely. Especially noting that in reality the systems not that much compete with one another as occupy different "ecological niches" and specialize for different areas and styles of work. Which addresses the last concern of the author, that mathematicians will have to adapt to a system designed for proving software correct and not mathematics. I have an impression that many proof assistants kinda "abandon" their "software correctness roots" for the glory of concurring Pure Math. 😁

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

WOW! That sounds HUGE! Extremely ambitious and exciting. Many right words, a number of unobvious insights. I wish them great success.

https://press.princeton.edu/books/paperback/9780691145990/how-mathematicians-think

"How Mathematicians Think: Using Ambiguity, Contradiction, and Paradox to Create Mathematics"

Sounds like serious fun! 😁

https://arxiv.org/pdf/2112.02142.pdf
An Impossible Asylum
Jeremy Avigad, Seulkee Baek, Alexander Bentkamp, Marijn Heule, Wojciech Nawrocki

In 1982, Raymond Smullyan published an article, “The Asylum of Doctor Tarr and Professor Fether,” that consists of a series of puzzles. These were later reprinted in the anthology The Lady or The Tiger? and Other Logic Puzzles. The last puzzle, which describes the asylum alluded to in the title, was designed to be especially difficult. With the help of automated reasoning, we show that the puzzle’s hypotheses are, in fact, inconsistent, which is to say, no such asylum can possibly exist.

Exposing mad scientists with the help of the Vampire! 🧛😁

By the way someone fixed something and Google Meet seems to work fine in Firefox again. I mean backgrounds and effects still don't but at least the main functionality works as before.

Ну и некоторая "выжимка" из этих приёмов визуализации была — снова значительное время назад — опубликована в блоге Stack Overflow: https://stackoverflow.blog/2022/03/03/stop-aggregating-away-the-signal-in-your-data/

#datascience #analysis #visualization

It was recommended to me, the book "Introduction to Statistical Learning":
https://hastie.su.domains/ISLR2/
and the lectures based on it:
https://www.youtube.com/watch?v=5N9V07EIfIg&list=PLOg0ngHtcqbPTlZzRHA2ocQZqB1D_qZ5V

The lectures seem pretty fun. 😊
#statistics #datascience #book #lectures

https://percival.ink/

It's essentially ObservableHQ, but with Datalog instead of JS while reusing the same plotting libraries. Genius.

#datascience #visualization #notebook

ADnD — Advanced Development and Delivery! 😂

DDnD — Development, Deployment and Delivery.