Understanding linear logic in five steps, purely computationally and without semantics.

We'll explain linear logic as a _specific_ self-interactive computational system by looking at more and more specific self-interaction computational systems until we arrive at classical linear logic.

CC @robpike.io

Ideas for a next generation text editor (Acme replacement):

1. Keep the Acme UI, but add rows, not just columns. Potentially make each window a full multiplexor (like rio(1), not 100% sure about this).

2. Make it multi-process/multi-machine again (like Sam, but better).

In a language that uses Curry-Howard you construct terms of some types, and the empty type denotes falsity.

I prefer programming *directly* with meanings (through types), and not indirectly through *codes*, what about you?

I am implementing CUE on top of interaction nets.

Partial evaluation seems to imply some degree of strictness and be at odds with lazy evaluation.

I have a specific counter example in mind but it's for a non-λ-calculus system. I don't know if inets guarantee β-optimality for all computational systems or just for λ-calculus.

I believe β-reduction in interaction combinators is not monotonic with respect to partial evaluation. In other words only program reduction (no free variables) is β-optimal. Is this true?

It’s funny how programmers not familiar with mathematics confuse types with sets, and mathematicians who don’t work in the foundations of mathematics confuse sets with types.

Types are not sets.