I love that Amiga emulators (FS/E/Win)UAE have an option to emulate the floppy drive sound. Very nostalgic, but also useful as an indication that something's happening!
7,969 karma · joined June 28, 2013
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.
Both Phosh and PlasmaMobile turn into a "proper" desktop when "docked" (Gnome-like and KDE-like, respectively).
That's made easier when writing (mostly) pure code, since the output is all we have (we're not mutating anything, or triggering other processes, etc. that would need extra checking).
I also think it's important to make sure we're checking the values we actually care about; since those might not be the literal return value of the "function under test". For example, if we're testing that some function correctly populates a table cell, I would avoid comparing the function's result against a hard-coded table, since that's prone to change over time in ways that are irrelevant. Instead, I would compare that cell of the result against a hard-coded value. (Rather than thinking about the individual values, I like to think of such assertions as relating one piece of code to another, e.g. that the "get_total" function is related to the "populate_total" function, in this way...).
The reason I find this important, is that breaking a test requires us to figure out what it's actually trying to test, and hence whether it should have broken or not; i.e. is it a useful signal that requires us to change our approach (the table should look like that!), or is it noise that needs its incidental details updated (all those other bits don't matter!). That can be hard to work out many years after the test was written!
I always feel obliged to point out that we can have 100% coverage without making a single assertion (beware Goodhart's law)
Indeed, I think of concepts like "agency", "choice", "free will", etc. as aspects of a particular sort of scientific model. That sort of model can make good predictions about people, organisations, etc. which would be intractable to many other approaches. It can also be useful in situations that we have more sophisticated models for, e.g. treating a physical system as "wanting" to minimise its energy can give a reasonable prediction of its behaviour very quickly.
That sort of model has also been applied to systems where its predictive powers aren't very good; e.g. modelling weather, agriculture, etc. as being determined by some "will of the gods", and attempting to infer the desires of those gods based on their observed "choices".
It baffles me that some people might think a model of this sort might have any relevance at a fundamental level.
It eschews angles entirely, sticking to ratios. It avoids square roots by sticking to "quadrances" (squared distance; i.e. pythagoras/euclidean-distance without taking square roots).
I highly recommend Wildberger's extensive Youtube channels too https://www.youtube.com/@njwildberger and https://www.youtube.com/@WildEggmathematicscourses
He's quite contrarian, so I'd take his informal statements with a pinch of salt (e.g. that there's no such thing as Real numbers; the underlying argument is reasonable, but the grand statements lose all that nuance); but he ends up approaching many subjects from an interesting perspective, and presents lots of nice connections e.g. between projective geometry, linear algebra, etc.
A couple of things I tend to notice:
- In magit, I can run a raw git shell commands by pressing `:`; majutsu doesn't seem to have that, so I use Emacs ordinary `M-!`
- The default view in majutsu (log) isn't as slick as magit's. With magit, I'll routinely open it up to look at the repo status, browse through the diffs (expanding/collapsing), staging/unstaging, etc. With majutsu, most of that requires first opening up the log, then opening up the diff of a commit.
- Staging/unstaging in magit is quite nice. The analogous workflow in jj seems to be splitting/squashing, but that feels clunkier in majutsu.
I've not opened bugs or PRs for these things, since it's mostly vibes and I don't have actual solutions to offer ;-)
EDIT: Oh, I also remembered that `jj` ignores $PAGER and uses its own built-in paging by default. That tries to act like `less`, and doesn't work well in Emacs. It can't use env vars either, unless we set its pager to something like `sh -c "$PAGER"` (see https://docs.jj-vcs.dev/latest/config/#pager ). Since my $PAGER is always `cat`, I've just set that as jj's pager directly too.
As someone who mostly lives in Emacs, I like it. If I'm away from a machine, I can SSH into it and carry on with whatever I was in the middle of.
It's also nice to set emacsclient as EDITOR, so that e.g. running `git commit` will open up a buffer in the existing Emacs session. This is especially useful since I use shell-mode, and it would be confusing/weird to have new Emacs instances popping up when I'm already in an editor! (They open in a "window" (i.e. pane) in the existing "frame" (i.e. window) instead)
For me, the best performance improvement has been handling long lines; e.g. Emacs used to become unusable if it was given a line of around 1MB. Since I run lots of shell-mode buffers, that would happen frustratingly-often. My workaround was to make my default shell a script that pipes `bash` through a pared-down, zero-allocation copy of GNU `fold`, to force a newline after hitting a certain length (crossing a lower threshold would break at the next whitespace; hitting an upper threshold would force a break immediately). That piping caused Bash to think it wasn't interactive, which required another work-around using Expect.
Thankfully the last few versions of Emacs have fixed long-line handling enough for me to get rid of my awful Rube-Goldberg shell!
I finally gave it a try when I came across the majutsu package, which is a magit-like interface for jujutsu. I recommend it for Emacs/magit users wanting to try `jj`!
Whilst lots of impressive things were built, the overall dream was always just out of reach. Domain-specific tooling is expensive to produce and maintain, and often gives something that's not quite what we want (as an extreme example, think of (X)HTML generated by Dreamweaver or FrontPage); generic XML processors/editors don't offer much beyond avoiding syntax/nesting errors; so often it was simplest to interact directly with the markup, where the verbosity, namespacing, normalisation, etc. wouldn't be automated-away.
XML's tree model was also leaky: I've worked with many data formats which look like XML, but actually require various (bespoke!) amounts of preprocessing, templating, dereferencing, etc. which either don't fit the XML model (e.g. graphs or DAGs), or just avoid it (e.g. sprinkling custom grammar like `${foo.bar}` in their text, rather than XML elements like `<ref name="foo.bar" />`). Of course, it was hard to predict how those systems would interact with XML features like namespaces, comments, etc. which made generic processing/transforming middleware less plug-and-play. That, plus billion-laugh mitigation, etc. contributed to a downward spiral of quality, where software would not bother supporting the full generality of XML, and only allowed its own particular subset of functionality, written in one specific way that it expected. That made the processors/transformers even less useful; and so on until eventually we just had a bunch of bespoke, incompatible formats again. At which point, many just threw up their hands and switched to JSON, since at least that was simpler, less verbose and easier to parse... depending whether you support comments... and maybe trailing commas...; or better yet, just stick to YAML. Or TOML.....
(My favourite example: at an old job, I maintained an old server that sent orders from our ecommerce site to third party systems, using a standard "cXML" format. Another team built a replacement for it, I helped them by providing real example documents to test with, and eventually the switch was made. Shortly after, customers were receiving dozens of times what they ordered! It turned out that a third-party was including an XML declaration like `<?xml>` at the start of their response, which caused the new system to give a parse failure: it treated that as an error, assumed the order had failed, and retried; over and over again!)
So, you're not surprised that this Om page has an extensive section called "Examples", right? https://www.om-language.com/#language__examples__
It seems pretty well done: when I added permission requests to the `bash` tool, the "Are you sure y/N" requests started appearing just like they were native to Emacs.
I agree. I tried Gemini CLI for a while, and didn't like how separate I felt from the underlying files: rather than doing minor cleanup myself, the activation energy of switching to a separate editor and opening the same files was too high, so I'd prompt the LLM to it instead. Which was often an exercise in frustration, as it would take many rounds of explanation for such tiny payoffs; maybe even fiddling with system prompts and markdown files, to try and avoid wasting so much time in the future...
I've been using Pi for a few weeks now, and have managed to integrate it quite deeply into Emacs. I run it entirely via RPC mode (JSON over stdio), so I don't really know (or care) about its terminal UI :-)
- Undecidability: that there are mathematical/logical questions whose answers cannot be calculated by any (formal/logical/physical) system
- Universal computation: there exist systems which can answer all decidable questions
- Universal Turing Machine: an incredibly simple example of such a universal system
Of course, these are inter-related and inevitable (otherwise they wouldn't be provable!); but at first glance it feels like these could have gone either way: Maybe all questions could be calculated, given sufficient cleverness (as Hilbert expected)? Maybe different systems would be required for different sorts of question? Maybe a universal system would be too outlandishly elaborate to make sense in our universe (as existence proofs often are)?
Yet here we are, discussing multiple ways to perform universal computation with GNU find!
The implementation is pretty terrible: a giant string of vibe-coded Emacs Lisp is sent to emacsclient, which performs the actions and sends back a string of JSON.
It's been interesting to iterate on the approach: watching the LLM (in my case Claude) attempting to use the tools; noticing when it struggles or makes incorrect assumptions; and updating the tool, documentation and defaults to better match those expectations.
I've also written some Emacs Lisp which opens Pi and tells it to "Action the request/issue/problem at point in buffer '<current-buffer>'" https://github.com/Warbo/warbo-emacs-d/blob/a13a1e02f5203476...
It feels similar to the file-watching provided by Aider (which uses inotify to spot files containing `# AI!` or `# AI?`), which I've previously used with FIXME and TODO comments in code; but it also works well in non-file things, e.g. error messages and test failures in `shell-mode`, and issues listed in the Emacs UI I wrote for the Artemis bug tracker (Claude just gets the issue number from the current line, and plugs that into a Pi extension I made for Artemis :-) )
The extensibility is really nice. It was easy to get it using my preferred issue tracker; and I've recently overridden the built-in `read` and `write` commands to use Emacs buffers instead. I'd like to override `edit` next, but haven't figured out an approach that would play to the strengths of LLMs (i.e. not matching exact text) and Emacs (maybe using tree-sitter queries for matches?). I also gave it a general-purpose `emacs_eval`, which it has used to browse documentation with EWW.
Pi supports permission popups, but doesn't use them by default. Their example extensions show how to do it (add an event listener for `tool_call` events; to block the call put `block: true` in its result).
> there's no secure way to know whether what they're asking to is what they'll actually do
What do you mean? `tool_call` event listeners are given the parameters of the tool call; so e.g. a call to the `bash` tool will show the exact command that will execute (unless we block it, of course).
That's how the pi-coding-agent Emacs package interacts with pi; and it's how I write automated tests for my own pi extensions (along with a dummy LLM that emits canned responses).
> I primarily wrote this package to navigate the command line help from kubectl and aws, both of which have nested sub-commands, and quite verbose (and helpful!) command line help.
> Neither of these programs ships with man pages, or similar offline documentation. I find myself consulting the command line help often, but struggling to find the experience very ergonomic.