hoping1

This and the other comment under this seem to be talking about the work the computer is doing at runtime. I believe the point is about the developer's work in implementing this. (For example, renaming potentially conflicting variables is clearly _less_ work than renaming only the actually conflicting variables, in this framing.) This kind of work is important for (1) compilers whose bugs are potentially very financially expensive, and (2) compilers with very intentionally-portable implementations (including but not limited to educational implementations)

See cvoss's comment in another thread:

" What happens in the evaluator when you have

(\ a . a a) (\ x . \ y . x y)

Variables are uniquely named at parse time, but after one beta step, you have two distinct instances each of x and y, albeit in different scopes, and after a second beta step, you have two distinct variables named y in the same scope. "

This doesn't come up in most mainstream languages, but Zig and Jai are getting people excited about comptime evaluation, and dependent types need comptime evaluation as well. Uniqueness is fine until you're doing higher-order evaluation in your compilation pipeline like this, which will be more and more desirable in the future, at least if the current trends are any indication.

An accessible introduction to the infamous Par operator, with a focus on intuition. Notably, this is on the broader concept of multiplicative disjunction, which appears even outside of linear logic!

Alternative title: Par and Constructive Classical Logic.

I've finally rounded out the Par trilogy, on sequent calculus, linear logic, and continuations! This post was the point of the whole series, and the most likely to contain things you haven't already heard. I really love par and the theory around it; the elegance is incredibly satisfying. I hope I can share that with you!

A new guide on linear logic! Much deeper than the usual "imagine a vending machine" guide, though I do mention the connection to that at the end lol. This is great for getting an intuition for substructural logics in academic papers, as well as the notorious multiple-conclusion sequents used in, say, type systems for safe parallelism. The post prior gives the necessary background on sequent calculus, if needed. This series is on much of the most beautiful theory ever, and I hope you enjoy!!

I'm glad you liked it! I have one more post planned for this series, on par and using continuations for classical logic proof terms. I have two other posts in the works but they aren't part of this series, which will only have that one more post. Much of what I learned was from blog posts like this one, or at least they got me to the point where I could understand the papers on my own. Blog posts, YouTube, reddit, discord, all helped me a ton. Originally I just wanted to make a cool programming language, but the more research I learned the more my interest shifted to the research, because it's just so unbelievably gorgeous and elegant!

Thanks!

A new guide on linear logic! Much deeper than the usual "imagine a vending machine" guide, though I do mention the connection to that at the end lol. This is great for getting an intuition for substructural logics in academic papers, as well as the notorious multiple-conclusion sequents used in, say, type systems for safe parallelism. The post prior gives the necessary background on sequent calculus, if needed. This series is on much of the most beautiful theory ever, and I hope you enjoy!!

Fair, I think of this as advanced logic, and those concepts (and that notation) as prerequisite.

Ah heck, I should have added a section on PTSs, maybe I still will or maybe that will be standalone later. It really is gorgeous stuff!!

Extensive and patiently-paced, with many examples, and therefore unfortunately pretty long lol