https://www.hillelwayne.com/post/algdt-history/
Turns out John McCarthy invented Algebraic Data Types and described their semantics in terms of finite sets. Also he (incidentally) was using the term spaces for the types. 😏
Turns out John McCarthy invented Algebraic Data Types and described their semantics in terms of finite sets. Also he (incidentally) was using the term spaces for the types. 😏
Hillel Wayne
A Very Early History of Algebraic Data Types
Been quiet around here! I’ve been putting almost all of my writing time into Logic for Programmers and my whole brain is book-shaped. Trust me, you do not want to read my 2000-word rant on Sphinx post-build LaTeX customization. But I spent the past week in…
🔥1
https://con.racket-lang.org/
October 4-5
Some very interesting talks, as per usual.
Online participation is possible, but costs like USD $10. Internet isn't free, after all. 😏
(fifteenth RacketCon)October 4-5
Some very interesting talks, as per usual.
Online participation is possible, but costs like USD $10. Internet isn't free, after all. 😏
AlexTCH
https://con.racket-lang.org/ (fifteenth RacketCon) October 4-5 Some very interesting talks, as per usual. Online participation is possible, but costs like USD $10. Internet isn't free, after all. 😏
Actually, that last bit is wrong:
The stream will be free to watch, but you can buy a ticket to support the conf.
The live stream is publicly available, but buying this ticket helps pay for the live stream and ensure its availability for the entire community.
The stream will be free to watch, but you can buy a ticket to support the conf.
🔥3
This is old, but still great news.
https://avehtari.github.io/ActiveStatistics/
Active Statistics by Andrew Gelman and Aki Vehtari
A #free introductory #book to (Applied) Statistics from some of the best teachers and practitioners of the craft alive. And that's not all what's great about it.
The book is unusual in that it's aimed at (university) teachers. And thus the material is split between two semester and weekly classes, while the first part explains the pedagogy of the book: the "flipped classroom" approach, the role of computation and simulation, setting up assessment, and so on.
The classes themselves are centered around "stories", which are supported by relevant activities for the students, computer demonstrations and open-ended questions to discuss.
Gelman was deeply thinking about what makes a good educational "story", and gave a couple of talks summarizing his conclusions and approach. Thus the stories in the book are far from random and purely entertaining anecdotes. They capture the essence of the topic and provide the bridge between more abstract statistical notions and techniques and the real-world applications.
While invaluable for teachers, the book is highly applicable for self-study or study group, as soon as you become your own teacher and can leverage the structure, examples and exercises.
https://avehtari.github.io/ActiveStatistics/
Active Statistics by Andrew Gelman and Aki Vehtari
A #free introductory #book to (Applied) Statistics from some of the best teachers and practitioners of the craft alive. And that's not all what's great about it.
The book is unusual in that it's aimed at (university) teachers. And thus the material is split between two semester and weekly classes, while the first part explains the pedagogy of the book: the "flipped classroom" approach, the role of computation and simulation, setting up assessment, and so on.
The classes themselves are centered around "stories", which are supported by relevant activities for the students, computer demonstrations and open-ended questions to discuss.
Gelman was deeply thinking about what makes a good educational "story", and gave a couple of talks summarizing his conclusions and approach. Thus the stories in the book are far from random and purely entertaining anecdotes. They capture the essence of the topic and provide the bridge between more abstract statistical notions and techniques and the real-world applications.
While invaluable for teachers, the book is highly applicable for self-study or study group, as soon as you become your own teacher and can leverage the structure, examples and exercises.
❤1
https://arstechnica.com/science/2025/09/meet-the-2025-ig-nobel-prize-winners/
Let's celebrate the victory march of Science!
Let's celebrate the victory march of Science!
https://www.youtube.com/watch?v=PnQ0eQrKF4g
Curious how our activities exert evolutionary pressure over various animal species, which gets recorded into their genes. Well, any activity on the planet exerts evolutionary pressure, that's the whole point. But humans act on unprecedentedly short time scales, and the nature notices (and adapts).
Curious how our activities exert evolutionary pressure over various animal species, which gets recorded into their genes. Well, any activity on the planet exerts evolutionary pressure, that's the whole point. But humans act on unprecedentedly short time scales, and the nature notices (and adapts).
YouTube
Animals Are Evolving to Survive in the Human World But Often in a Weird Way
Support this channel on Patreon to help me make this a full time job: https://www.patreon.com/whatdamath (Unreleased videos, extra footage, DMs, no ads)
Alternatively, PayPal donations can be sent here: http://paypal.me/whatdamath
Get a Wonderful Person Tee:…
Alternatively, PayPal donations can be sent here: http://paypal.me/whatdamath
Get a Wonderful Person Tee:…
❤1
https://www.answer.ai/posts/2025-06-05-readbench.html
The folks designed and implemented the
The results are kinda as expected, but still show that you can't simply pile all of your scanned documents into a DB and expect a VLM to efficiently sift through them all and extract necessary information.
The folks designed and implemented the
ReadBench benchmark for testing Vision-Language Models (VLMs) and other Multimodal LLMs essentially on the OCR tasks.The results are kinda as expected, but still show that you can't simply pile all of your scanned documents into a DB and expect a VLM to efficiently sift through them all and extract necessary information.
Answer.AI
TIL: Vision-Language Models Read Worse (or Better) Than You Think – Answer.AI
Introducing ReadBench, a straightforward way to see how well your favorite Vision-Language Models read text-rich images.
https://julialang.org/blog/2025/10/julia-1.12-highlights/
Julia 1.12 is out. This one largely continues the long-standing theme of improvements to compilation and packaging.
Compilation improvements include the option to build the Julia itself with LLVM BOLT (as well as LTO and PGO), and precompilation times tracing.
For building self-contained binary images there's now an expreimental option to
Other packaging improvements include support for workspaces comprising several closely related projects (like a library + tests + benchmarks + docs + examples) and dedicated (CLI) apps.
Julia 1.12 is out. This one largely continues the long-standing theme of improvements to compilation and packaging.
Compilation improvements include the option to build the Julia itself with LLVM BOLT (as well as LTO and PGO), and precompilation times tracing.
For building self-contained binary images there's now an expreimental option to
--trim all statically unreachable code, which yields way smaller binaries, but (expectedly) breaks on dynamic dispatches and other dynamic features. Looks very similar to AOT compilation for Java and C# which also breaks on reflection and similar dynamic features.Other packaging improvements include support for workspaces comprising several closely related projects (like a library + tests + benchmarks + docs + examples) and dedicated (CLI) apps.
julialang.org
Julia 1.12 Highlights
Highlights of the Julia 1.12 release.
🔥1
This year’s London Mathematical Society (LMS) / British Computer Society -- Formal Aspects of Computing Science (BCS-FACS) Evening Seminar will feature Jeremy Avigad as the distinguished speaker. Registration is free but required in advance.
https://www.lms.ac.uk/events/lms-bcs-facs-seminar-jeremy-avigad
Date: 6 November 2025
Time: 19:00 (UK time)
Format: Online via Zoom
Talk title: Mathematics in the Age of AI
Abstract:
New technologies for reasoning and discovery are bound to have a profound effect on mathematical practice. Proof assistants are already changing the nature of collaboration, communication, and curation of mathematical knowledge. Automated reasoning tools are used to find mathematical objects with specified properties or rule out their existence, and to decide or verify mathematical claims. Machine learning and neural methods can discover patterns in mathematical data, explore complex mathematical spaces, and generate mathematical objects of interest. Neurosymbolic theorem provers, now capable of solving the most challenging competition problems, combine aspects of all of these technologies.
It is helpful to keep in mind that the phrase "AI for mathematics" encompasses several distinct technologies that overlap and interact in interesting ways. In this talk, I will survey the landscape, describe a few landmark applications to mathematics, and encourage you to join me in thinking about how mathematicians and computer scientists can collaborate to guide mathematics through this era of technological change.
The talk shall be uploaded to YouTube as well as the previous ones:
https://www.youtube.com/channel/UCvp7jsbXjx2k8sGEkdtWCAw
https://www.lms.ac.uk/events/lms-bcs-facs-seminar-jeremy-avigad
Date: 6 November 2025
Time: 19:00 (UK time)
Format: Online via Zoom
Talk title: Mathematics in the Age of AI
Abstract:
New technologies for reasoning and discovery are bound to have a profound effect on mathematical practice. Proof assistants are already changing the nature of collaboration, communication, and curation of mathematical knowledge. Automated reasoning tools are used to find mathematical objects with specified properties or rule out their existence, and to decide or verify mathematical claims. Machine learning and neural methods can discover patterns in mathematical data, explore complex mathematical spaces, and generate mathematical objects of interest. Neurosymbolic theorem provers, now capable of solving the most challenging competition problems, combine aspects of all of these technologies.
It is helpful to keep in mind that the phrase "AI for mathematics" encompasses several distinct technologies that overlap and interact in interesting ways. In this talk, I will survey the landscape, describe a few landmark applications to mathematics, and encourage you to join me in thinking about how mathematicians and computer scientists can collaborate to guide mathematics through this era of technological change.
The talk shall be uploaded to YouTube as well as the previous ones:
https://www.youtube.com/channel/UCvp7jsbXjx2k8sGEkdtWCAw
👍1
To whom it might concern. There's the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM):
https://popl26.sigplan.org/series/pepm
There's still some time to send a paper to the 2026 instance.
https://popl26.sigplan.org/series/pepm
There's still some time to send a paper to the 2026 instance.
popl26.sigplan.org
PEPM conference series - PEPM 2026
The ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM) has a history going back to 1991 and has been held in conjunction with POPL every year since 2006. The origin of PEPM is in the discoveries of practically useful automated techniques…
The Computing Science division at the University of Gothenburg has a 360 days research position to work with Prof. Thierry Coquand and his group.
Deadline for application is Oct 30th.
The project is about the study of dependent type theory extended with univalence with applications to synthetic mathematics. Prime examples are synthetic algebraic geometry and synthetic Stone duality, but it might be other kind of synthetic mathematics, such as study of higher categories.
https://web103.reachmee.com/ext/I005/1035/job?site=7&lang=UK&validator=9b89bead79bb7258ad55c8d75228e5b7&job_id=38480
PhD is required. 😏
Deadline for application is Oct 30th.
The project is about the study of dependent type theory extended with univalence with applications to synthetic mathematics. Prime examples are synthetic algebraic geometry and synthetic Stone duality, but it might be other kind of synthetic mathematics, such as study of higher categories.
https://web103.reachmee.com/ext/I005/1035/job?site=7&lang=UK&validator=9b89bead79bb7258ad55c8d75228e5b7&job_id=38480
PhD is required. 😏
Reachmee
Researcher in type theory for mathematics and computer science
The department of Computer Science and Engineering is strongly international, with approximately 300 employees from
A Summer School in December! Welcome to Australia:
https://comp.anu.edu.au/lss/
This year the focus is on Modal Logics and Type Theories, and software verification in Isabelle/HOL.
https://comp.anu.edu.au/lss/
This year the focus is on Modal Logics and Type Theories, and software verification in Isabelle/HOL.
Logic Summer School @ANU
33rd Annual Logic Summer School @ANU
Homepage of the Logic Summer School program at ANU School of Computing.
https://github.com/CharlesCNorton/intel-4004-verified
🔥
Formal Verification of the Intel 4004 Microprocessor in Coq
🔥
GitHub
GitHub - CharlesCNorton/intel-4004-verified: Formalizing the Intel 4004 microprocessor
Formalizing the Intel 4004 microprocessor. Contribute to CharlesCNorton/intel-4004-verified development by creating an account on GitHub.
🔥2😁1
They formalized (and mechanized) the https://en.wikipedia.org/wiki/Z_notation in Isabelle/HOL:
https://www.isa-afp.org//entries/Z_Toolkit.html
Finally a decent IDE and proof automation for Z. 😏
https://www.isa-afp.org//entries/Z_Toolkit.html
Finally a decent IDE and proof automation for Z. 😏
👍1🔥1
https://trop.in/blog/i-have-to-live-in-a-forest-to-work-on-open-source
It doesn't cover all the details and nuances, but still. That's how life happens to some of us.
It doesn't cover all the details and nuances, but still. That's how life happens to some of us.
trop.in
I Have to Live in a Forest to Work on Open Source — Andrew Tropin
https://www.laser-foundation.org/verifai-26/
The VERIFAI workshop, the first of its kind, is devoted to the interplay between the two technologies: not only how to verify AI tools but also (the main focus) how verification techniques can make “vibe coding” efficient and reliable.
20 December 2025: submission deadline for full papers (max 15 pages) or extended abstracts (2 to 5 pages) for participation in the workshop.
8-11 March 2026: workshop
The VERIFAI workshop, the first of its kind, is devoted to the interplay between the two technologies: not only how to verify AI tools but also (the main focus) how verification techniques can make “vibe coding” efficient and reliable.
20 December 2025: submission deadline for full papers (max 15 pages) or extended abstracts (2 to 5 pages) for participation in the workshop.
8-11 March 2026: workshop