In classical logic, bindings are inexhaustible, if a formula proves something from x, you can use x ten times, or zero times, it doesn’t matter. But programming doesn’t work like that, resources do matter. I don't say this to mean that copying a register is costing cycles, but that semantically speaking, closing a file or freeing memory should consume the access to that resource.

In catlangs, bindings are fuel, if you want two copies, you must duplicate. It becomes an operation, not a ambient assumption. Jean-Yves Girard wrote extensively about this, and his insight was that this linear logic was closer to reality, it makes logic reflect process. In other words, traditional logic is static and he wanted a logic of change.

I see #Forth thrown left and right around #permacomputing circles on vague notions of efficiency and human-scaleness, but I think what lies beneath these intuitions is that classical logic assumes infinite copyability. Which is unrealistic for memory, energy and just about any physical system. Linear logic, which is found at the heart of stack machines, says that duplication is not free, erasure is not free, both must be explicit. This conservation law aligns logic with a finite natural world.

Programming languages typically hide duplication and lifetimes, or tack helpers on top as an afterthought. Values duplicate freely, things exist everywhere at once, names abstract away placement, this may activate one's linguistic thought process but keep the spatial system asleep. My experience with catlang has had less to do with fussing with names and symbols and more to do with something like weaving. On this loom, things don't have names but occupy spaces in a braid over time. If I had to guess, I'd say that probably triggers the same geometrically thinking part of the brain that tracks physical objects.

And that's the unique bit about catlangs!

wiki.xxiivv.com/site/now