The only thing I've noticed is that `jj` will leave the git repo with either a detached HEAD, or with a funny `@` ref checked out.

I don't think that would trouble someone who's experienced with git and knows its "DAG of commits" model.

For someone who's less experienced, or only uses git for a set of branches with mostly linear history (like a sort of "fancy undo"), I could imagine getting a shock when trying to `git commit` and not seeing them on any of the branches!

jj doesn't "want" anything.

I always end a piece of work with `new`: it puts an empty, description-less commit as the checked-out HEAD, and is my way of saying "I'm finished with those changes (for now); any subsequent changes to this directory should go in this (currently empty) commit"

The last thing I do to a commit, once all of its contents have settled into something reasonable, is describe it.

In fact, I mostly use `commit` (pressing `C` in majutsu), which combines those two things: it gives the current commit a description, and creates a new empty commit on top.

I do that all the time. With git, everything starts "unstaged", so I'd use magit to selectively stage some parts and turn those into a sequence of commits, one on top of another.

With jj I'd do it "backwards": everything starts off committed (with no commit message), so I'd open the diff (`D` in majutsu), selecting some parts and "split" (`S` in majutsu) to put those into a new commit underneath the remaining changes. Once the different changes are split into separate commits, I'd give each a relevant commit message.

Now let's say the output looks wrong; e.g. we get nothing out. Weird, the previous command looked right, and it doesn't seem to be a problem with the filter we just put on the end. Maybe the filter we added part-way-through was discarding too much, so that the things we actually wanted weren't reaching the later stages; we didn't notice, because everything was being drowned-out by irrelevant stuff that that our latest filter has just gotten rid of.

Tricks like this `\#` let us turn off that earlier filter, without affecting anything else, so we can see if it was causing the problem as we suspect.

As for more general "why use CLI?", that's been debated for decades already; if you care to look it up :-)

You also mention there being "little value", when your proposed approach costs literal money in form of API/token usage (when using hosted models).

> Now I've moved to coding in Haskell

You might like https://hackage.haskell.org/package/turtle or http://nellardo.com/lang/haskell/hash/

This will output the stdout of mycmd1:

    mycmd1 #| mycmd2 | mycmd3

    mycmd1 | \# mycmd2 | mycmd3

Maybe I'm misunderstanding you, but Curry-Howard is a mapping between mathematical jargon and programming jargon, where e.g. "this is a proof of that proposition using foo logic" maps to "this program has that type in programming language foo".

I don't see how that makes "binaries" a "full-fidelity mathematical model": compilation is (according to Curry-Howard) translating a proof from one system of logic to another. For a binary, the resulting system of logic is machine code, which is an absolutely terrible logic: it has essentially one type (the machine word), which makes every proposition trivial; according to Curry-Howard, your database binary is proof of the proposition corresponding to its type; since the type of every binary is just "some machine words", the proposition that your database binary is a "full-fledged mathematical model" of is essentially just "there exists a machine word". Not very useful; we could optimise it down to "0", which is also a proof that there exists a machine word.

If we assume that you want to prove something non-trivial, then the first thing you would need to do is abstract away from the trivial logic of machine code semantics, by inferring some specific structures and patterns from that binary, then developing some useful semantics which captures those patterns and structures. Then you can start to develop non-trivial logic on those semantics, which will let you state worthwhile propositions. If we apply the Curry-Howard lens to that process, it corresponds to... decompilation into a higher-level language!

tl;dr Curry-Howard tells us that binaries are literally the worst possible representation we could hope for.

There have been simplistic attempts at this, e.g. instead of performing 100 tests, just keep going as long as coverage increases.

The Choice Gradient Sampling algorithm from https://arxiv.org/pdf/2203.00652 feels like a nice way to steer generators in a more nuanced way. That paper uses it to avoid discards when rejection-sampling; but I have a feeling it could be repurposed to "reward" based on new coverage instead/as-well.

I disagree. Having tests (even if the LLM wrote them itself!) gives the model some grounding, and exposes some of its inconsistencies. LLMs are not logically-omniscient; they can "change their minds" (next-token probabilities) when confronted with evidence (e.g. test failure messages). Chain-of-thought allows more computation to happen; but it doesn't give the model any extra evidence (i.e. Shannon information; outcomes that are surprising, given its prior probabilities).

At the risk of stretching the analogy, the LLM's internal representation is that theory: gradient-descent has tried to "explain" its input corpus (+ RL fine-tuning), which will likely contain relevant source code, documentation, papers, etc. to our problem.

I'd also say that a piece of software is a theory too (quite literally, if we follow Curry-Howard). A piece of software generated by an LLM is a more-specific, more-explicit subset of its internal NN model.

Tests, and other real CLI interactions, allow the model to find out that it's wrong (~empiricism); compared to going round and round in chain-of-thought (~philosophy).

Of course, test failures don't tell us how to make it actually pass; the same way that unexpected experimental/observational results don't tell us what an appropriate explanation/theory should be (see: Dark matter, dark energy, etc.!)

I see what you mean w.r.t. different hats; but is it useful to have different tools available? For example, a "planner" having Web access and read-only file access, versus a "developer" having write access to files but no Web access?

This seem to be completely subjective; I write syntactically/grammatically "nice" sentences to LLMs, because that's how I write. I would have to "invest energy" to force myself to write in that supposedly "simpler" style.