camilochs

I rewrote it. The "how young this is" section is gone, and the design section is now in my own words. Thanks for the push!

The thing is, my goal was to enhance the text editor and improve the error messages, but not to abandon TeX. That's the price I have to pay.

I added types because I wanted a better text editor for LaTeX; I was tired of using Overleaf, so I created Vitela (https://vitela.artificialfallibility.com/). Types provide me with useful information before compiling, similar to what TypeScript does with JavaScript.

Types are just the mechanism. The real problem is the one fph pointed out: LaTeX reports errors in its own terms instead of the author’s, and review comments live somewhere else. Gradual typing is simply how the compiler can understand the names you introduce without pretending that all of LaTeX can be typed, because it can't.

It does not take some other language and compile it down to LaTeX. LaTeX itself is the source, and it goes through unchanged. What ExactTeX adds is a layer of checks and diagnostics based on the names and annotations you introduce. If anything, AI-assisted writing makes that layer even more valuable. Agents can generate LaTeX quickly, but they also make mistakes quickly, and an error like "Missing } inserted" is no more helpful to an agent than it is to a human.

I agree that Typst is nicer to write. The difference is simply in the approach. Typst replaces LaTeX and expects you to migrate, while ExactTeX is a strict superset. You can rename a `.tex` file to `.xtex`, keep the exact same output, and add checks only where you need them. It is meant for the existing papers, templates, and journal classes that are not going away. Typst works well if you can leave LaTeX behind. ExactTeX is for cases where you cannot or do not want to.

Yes, Claude, good ear :) The compiler was built with agents; the repo has an AGENTS.md describing how they're used. Without them this would have taken me months instead of days. But the design is mine, and so are the mistakes. The decisions that shape the whole thing, byte-for-byte compatibility with existing .tex, gradual typing with an explicit unknown (`?O`) instead of trying to type all of LaTeX, and review comments living inside the file, come from years of writing papers in Overleaf and wanting more from the compiler than "Missing } inserted". Vitela (https://vitela.artificialfallibility.com/) exists because once the compiler knows more, the editor can show it. Fair hit on the prose, though. I'll rewrite that section myself.

Researcher in distributed systems, and lead author of the book Distributed Systems.

Lambda calculus is a formal notation that enables the expression of computable functions. It serves as the foundation for functional programming and is defined using the Greek letter lambda (λ). It is expressed through lambda expressions and lambda terms, which are used to represent binding variables within a function. This document aims to provide a basic introduction to the theoretical and practical aspects of lambda calculus and functional programming. For the latter, we will utilize the Racket programming language.

Conversations with Brian Kernighan, Bjarne Stroustrup, Alfred Aho, Leslie Lamport, among others. The English version can be found at the end of each interview.

A book about lambda calculus and functional programming using Racket and Python.

I did update the code. thank you