Carlo Angiuli

@danielgratzer@mathstodon.xyz and I have just released a new version of Principles of Dependent Type Theory! This one is a significant milestone: all planned content has been drafted; we do not expect any new sections at this point.

Main changes:

• Added Appendix B on generalized algebraic theories! This resolves some unfinished business from earlier in the book, by proving the "initiality theorem" for ETT/ITT.
• Added a draft of Section 4.4 on observational type theory.
• Removed "solutions to selected exercises", and converted the most important handful of exercises into lemmas with proofs.
• Various improvements to Chapter 6 (categorical semantics).
• Expanded Section 3.6 on undecidability of equality in ETT, including a series of exercises establishing the undecidability of equality in TT with judgmental Nat-eta.

https://www.carloangiuli.com/papers/type-theory-book.pdf

In a previous wave of Lean discourse, there was discussion about the fact that type-checking a Lean file can run arbitrary code. There are pros and cons to this, but one particularly obvious con is, well, let's just hear Kevin Buzzard's version:

"One cannot trust AI-generated code so I ran [the AI-generated formalization of the Erdős unit distance conjecture counterexample] in a sandbox on my machine (malicious Lean code can run arbitrary commands on your computer — Lean is a programming language, after all)." (https://xenaproject.wordpress.com/2026/07/20/human-mathematicians-are-being-outcounterexampled/)

My beloved LaTeX is another example of a tool in which you can write arbitrary code that generates a document of some kind, but in this case it can only do real damage if you pass the `--shell-escape` flag.

As far as I can tell, Lean doesn't have an equivalent "sandboxed" mode. Am I missing something? Why isn't this something people want?

RE: @danielgratzer@mathstodon.xyz

We are working together in Daniel’s office, and every time his computer dings with another like on this post, he looks at me like 😏

LICS paper with @trebor@types.pl accepted! 🎉

Went to lunch today with the PL grad students, who started discussing their relatively large range of ages.

Student 1: Well, I'm 24.
Me: I mean, isn't that the age Coolio said he wasn't sure if he'd live to see?
Student 2: Who's Coolio?
Student 3: That's a musical artist, right?
Student 2: ...from the 1900s?
[@samth@mastodon.social and I are dying]

PCF is a domain-specific language for ω-cppos.

17th century mathematical mistakes: I have a proof that is too large to fit in this margin.

21st century mathematical mistakes: I have a file that is too large to fit in this buffer.

@totbwf

In particular, we put some indexed inductives in Typeω to avoid generating the extra cubical code.

lmao.

@stschaef @amy @ncf