reuben364

The quote you gave seems reasonable on it's own. ICE and Palantir comes to mind as exactly the kind of thing one would want to avoid. Could you elaborate on what particularly you find lacking in that quote?

I find that at the granularity you need to work with current LLMs to get a good enough output, while verifying its correctness is more effort than writing code directly. The usefulness of LLMs to me is to point me in a direction that I can then manually verify and implement.

I was surprised to not see a connection made to free groups in the article.

EDIT: The wikipedia article that is.

I'm wondering whether such syntax is subsumed by something like Lean 4 macros. I believe Lean 4 already treats binders specially in its syntax for macro hygiene reasons, but I'm not confident in that assertion.

Since the de Bruijn indices are limited (and presumably still Turing complete), I wonder how limited you can make them and still be Turing complete.

I just wrote redef to emphasize that I'm not shadowing the original definition.

    def a := 1
    def f x := a * x
    -- at this point f 1 evaluates to 1
    redef a := 2
    -- at this point f 1 evaluates to 2

But with dependent types, types can depend on prior values (in the previous example the type of x depends on the value t in the most direct way possible, as the type of x is t). If you redefine values, the subsequent definitions may not type-check anymore.

Thinking out aloud here.

One pattern that I have frequently used in EMACS elisp is that redefining a top-level value overwrites that value rather than shadowing it. Basically hot reloading. This doesn't work in a dependently typed context as the type of subsequent definitions can depend on values of earlier definitions.

    def t := string
    def x: t := "asdf"
    redef t := int

redefining t here would cause x to fail to type check. So the only options are to either shadow the variable t, or have redefinitions type-check all terms whose types depend on the value being redefined.

Excluding the type-level debugging they mention, I think a lean style language-server is a better approach. Otherwise you are basically using an append-only ed to edit your environment rather than a vi.

There is a large library of mathematics formalized in lean called mathlib. There are graphs for the module dependencies, but I haven't seen any at the level of definitions (including lemmas and theorems).

It matters for anti-circumvention, where they can go after people that make tools that allow you to make personal copies.

Not sure of details to make it a mathematical foundation but:

A category can be defined in terms of its morphisms without mentioning objects and a topos has predicates as morphisms into the subobject classifier.

That'd almost be partial functions with extra steps. Take the Klesili category with the Maybe Monad,and you get partial functions.

Unless you are manually matching on the the Maybe, and thus observing the timeout, then that isn't the case. You'd probably also want a nondetermism effect which cannot handle unless you specifically build your timeouts to be deterministic, which I think Lean 4 does, but you can't go from partial to total with it afaik.

a function will return to it's call site (or diverge), a handler doesn't necessarily have to resume from where it was invoked. There is also (sort of) dynamic scoping, where you don't have to thread the handlers through calls.

I'm left confused as to what the gluing in the rule replacement is. Must the boundary of a rule match on both sides? Also what examples there would be of what an example would of having topology that is not induced from a graph if it is at all possible.