Aram Hăvărneanu @xw.is · 07/09/2025Our computational system is now a _symmetric monoidal system with identities_. 000
Aram Hăvărneanu @xw.is · 07/09/2025While the multiplicatives units were about creating resources out of nothing, the additive units are about _computations_ out of nothing. That's why their utility is relegated to discharging _impossible_ hypotheticals. 100
Aram Hăvărneanu @xw.is · 07/09/2025Step 5: 0, ⊤ The multiplicatives have units, it makes sense to ask whether the additives can also have inverses. Indeed we can add them as 0, ⊤. 100
Aram Hăvărneanu @xw.is · 07/09/2025The penultimate step is convincing yourself that the rules of the linear logic are precisely the ones which _self-dual under completion_. That is, the rules that can produce the richest states (most states) while being dual. 100
Aram Hăvărneanu @xw.is · 07/09/2025Step 4: the dualities What we've said so far was without looking (too much) at the _specific_ interaction rules. 100
Aram Hăvărneanu @xw.is · 07/09/2025We accept that, of course, _global_ things can simply exist independently of _local_ computation. The interaction rules are still local, however there is global state unperturbed by local interaction. 100
Aram Hăvărneanu @xw.is · 07/09/2025Step 3: ?, ! We add the exponentials: ?, !. Whereas before we could only refer to transient state, now we can refer to _perennial, stable state_. 100
Aram Hăvărneanu @xw.is · 07/09/2025Here, state is ephemeral. Whatever this state means (if anything at all), is but a _transient state of an evolving system_. The system can visit a state multiple times, of course, but it has to create it every time (and at this point it can only visit a state a finitely number of times anyway). 100
Aram Hăvărneanu @xw.is · 07/09/2025Because we can make and eliminate things, the dynamics of the possible computational becomes more interesting. In particular we don't need extra-logical initial state. 100
Aram Hăvărneanu @xw.is · 07/09/2025Unlike what we had before, which was a set of _fixed_, conserved resources, we can make 1 out of nothing. The set of resources is now _dynamic_. 100
Aram Hăvărneanu @xw.is · 07/09/2025Step 2: 1, ⊥ We add 1, ⊥. These allow making the resources and some of the rules we had before (the multiplicatives) in a monoid. This is useful. 100
Aram Hăvărneanu @xw.is · 07/09/2025The axiom rule is kinda like a "virtual particle". It can split from nothing into complementary hypothesis, but ultimately it doesn't _do_ anything, merely its "branches" enable other resources to interact via cuts. We need the initial state to really make anything interesting happen. 100
Aram Hăvărneanu @xw.is · 07/09/2025Also note that we have a bit of a bootstrapping problem here. Where do the resources come from? They initial state had to be given to us "extra-logically". 100
Aram Hăvărneanu @xw.is · 07/09/2025Don't worry about what these resources are, or why the rules are what they are (we'll come back to the specific rules later). Simply observe the symmetry of the rules and internalize the "conservation principle" implied by the computational rules. 100
Aram Hăvărneanu @xw.is · 07/09/2025The specific arrangement of resources using ⊗, ⅋, ⊕, & form a _state_, and the rules tells us how the state _evolves_. 100
Aram Hăvărneanu @xw.is · 07/09/2025Step 1: ⊗, ⅋, ⊕, & We're given a finite set of locally-interacting resources. All of them get preserved by interaction. The interaction rules pack and unpack resources using funny-looking symbols: ⊗, ⅋, ⊕, &. 100
Aram Hăvărneanu @xw.is · 07/09/2025Here we're doing something else, we'll be talking _only_ about the computational content of _sequent calculus itself_, not of any logic contained therein (here, linear logic). Let's begin. 100
Aram Hăvărneanu @xw.is · 07/09/2025Note that when doing Curry-Howard correspondence we're necessarily internalizing logical deduction into internal connectives. For example, we can make a function-an internal object in the theory—out of a meta-level statement (sequent entailment). 100
Aram Hăvărneanu @xw.is · 07/09/2025Understanding 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. 100
Aram Hăvărneanu @xw.is · 13/05/2025Because the selection is sticky, you can have B2-execute and B3-search, just don't modify it! A click+release can have the exact same behavior (even if a menu is appears during on-click). 100
Aram Hăvărneanu @xw.is · 13/05/2025Of course, keep what is already great: 16. No settings, no options, no themes, no syntax highlighting, no keyboard based interface (the mouse is king). 100
Aram Hăvărneanu @xw.is · 13/05/202514. Elastic tab support, or some better way of dealing with tabular data. 15. A better way of dealing with resize, right now acme does really bad when moving from a big monitor to a laptop because it preserves layout. I'd like a way to globally set layout independent of Dump. 100
Aram Hăvărneanu @xw.is · 13/05/2025This should be done by a third party process writing in acme(4), acme(1) should not implement native markdown support or anything like that. 100
Aram Hăvărneanu @xw.is · 13/05/202513. Some sort of minimal markup support. Perhaps with colors. Not arbitrary colors, just like four or five predetermined colors that Acme programs could make use of (for example I'd like to see colors in my diffs). 100
Aram Hăvărneanu @xw.is · 13/05/202512. Multiple window support, in the sense of multiple operating system windows. 200
Aram Hăvărneanu @xw.is · 13/05/202511. Unlike in Plan 9, where paths are short (because you have namespaces), in Unix paths are long (because people have poor taste). This is annoying to deal with in Acme ATM, but I'm not sure what the right design for a solution is. 200
Aram Hăvărneanu @xw.is · 13/05/202510. A better way to place commands that you'd put in the tag, perhaps B2 opens a persistent window for window-specific (not global) commands. 100
Aram Hăvărneanu @xw.is · 13/05/20258. Add support for space-based indentation. Disgusting, but necessary (I patched my acme to support this, but it still requires manual activation, should be automatic). 100
Aram Hăvărneanu @xw.is · 13/05/20257. Expand the span for B3 auto-selection to include software that doesn't use `file:line:col` convention. Of course the plumber can do this, but it requires a manual B3 selection, auto-selection has to work. 110
Aram Hăvărneanu @xw.is · 13/05/20255. Add enough ANSI terminal sequences support to win(1) such that workarounds are no longer necessary for common CLI software (git(1), grep(2), etc). 6. Replace structural regular expression with something based on Tree-sitter, but with an actual usable syntax. 100
Aram Hăvărneanu @xw.is · 13/05/20253. Add a Sam-like menu on B2/B3. It should work like Sam (last used selection is default), but behave more like Octopus/Plan B (star-like expansion). This can make use of mouse gestures, no need to click twice. 4. Add support for mouse hover. 200
Aram Hăvărneanu @xw.is · 13/05/2025Ideas 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). 100
Aram Hăvărneanu @xw.is · 23/03/2025`x: 3` is not a proof that x equals 3, rather it is an existential statement that says that x can't be assumed to be anything else than 3. The latter can be refuted, say by `x: 2`, in which case x is actually ⊥. 000
Aram Hăvărneanu @xw.is · 23/03/2025And I say plausible instead of possible, because CUE is consistent and reflective. This means it can't be complete. 100
Aram Hăvărneanu @xw.is · 23/03/2025CUE is a logic of plausible axiomatic consistency. There are no proofs, there is just the admissibility of future refutation of existential statements. 100
Aram Hăvărneanu @xw.is · 23/03/2025In a co-program that has not completed, it is not so much that types are not empty, it's that they might be non-empty. As long as their inhabitance is still possible, the program doesn't stop. 100
Aram Hăvărneanu @xw.is · 23/03/2025In CUE, you only build types (every term is its own type), and you build them destructively by chipping away at them. What you build are co-programs, not programs, and the only certain type is the empty type. Arriving at the empty type marks the completion of the program. 110
Aram Hăvărneanu @xw.is · 23/03/2025In a language that uses Curry-Howard you construct terms of some types, and the empty type denotes falsity. 100
Aram Hăvărneanu @xw.is · 19/03/2025Programming with meanings is really just programming in a way where programs are constrained to produce meaningful results. Programming with meanings means programming with types. 100
Aram Hăvărneanu @xw.is · 19/03/2025Soundness and adequacy still hold, just without full abstraction. This is still an incredibily strong property. Plus in practice, all useful programs are terminating (see Danielsson et al., Fast and loose reasoning is morally correct, doi.org/10.1145/1111...). 100
Aram Hăvărneanu @xw.is · 19/03/2025If your type system is weaker and admits empty types (Curry-Howard doesn't strictly hold) then your encoding function (identity) is only a partial function. In this case your type system only provides the preservation of meaning, and not the guarantee of meaningfulness. 100
Aram Hăvărneanu @xw.is · 19/03/2025But because of the bijection between object-level types and meta-theoretical types — between object-level types and types that describe meaning — object-level type safety implies the preservation of meaning *whatever the meaning is*. 100
Aram Hăvărneanu @xw.is · 19/03/2025*2. Programming languages are oblivious to meaning.* Programming languages are (hopefully) concerned with type safety, that is object-level types. 100
Aram Hăvărneanu @xw.is · 19/03/2025Quite different than working with codes, of which the correctness depends on meta-level properties and realizability semantics. 100
Aram Hăvărneanu @xw.is · 19/03/2025So to answer the original question, yes, there is an encoding, but it's an encoding that is 1. simple (trivial type-level map using only simple types), 2. meaningful (it's *about* meaning), 3. safe (correctness depends only on object-language properties). 100
Aram Hăvărneanu @xw.is · 19/03/2025(As an aside, whether you prefer to think in terms of a bijection or in terms of an identity corresponds to whether you prefer universes à la Tarski, or universes à la Russell.) 100
Aram Hăvărneanu @xw.is · 19/03/2025Yes, it's just the identity function. *That's it*. That's the encoding. Understanding what just happened here is the key to the understanding what types really are. 100
