Clojurians Log v2

🧵 Under the hood. The optimizer is an e-graph (equality-saturation, egg-style) rewriter: it builds out the space of forms your pipeline is provably equal to under the rule set, then extracts the cheapest — each adopted rewrite carrying its kernel proof. Same idea as a modern query optimizer, except the rewrites are certified and the IR is your pipeline. It also plans jointly with datahike and stratum: embed a d/q or stratum query right in a pipeline and the planner optimizes across the boundary — pushing the aggregation through the join, factorizing, choosing the drive direction — so the same planning + optimized execution those engines bring to your queries reaches the code around them too. Extending it to your domain: the rewrite rules are just kernel-checked laws. Have a coding assistant add the laws for your operators (a custom fold, a domain join, a bespoke aggregation); once they're in, every pipeline that uses them gets planned automatically — even as you keep editing.

ansatz 0.2 — "Verified Clojure via Lean 4" — the kernel + DSL underneath (and what the assistant uses to check the rules it writes), now much easier to pick up. If you already write malli-instrumented Clojure, it's the gradual next step — keep your schema, change defn → a/defn:

clojure
(require '[ansatz.core :as a] '[malli.core :as m])
(a/load-init!)                          ; bundled Lean Init, zero setup (straight from the jar)

(m/=> dbl [:=> [:cat :int] :int])       ; just a malli schema
(a/defn dbl [x] (+ x x))                ; defn → a/defn — now machine-checked, still plain Clojure
(dbl 21)                                ; => 42

Yo @whilo do you generate these announcements with an LLM?

I am working with Claude models mostly, yes. Why, is it confusing/misleading? I am drafting, iterating and reading what I publish and find having a drafting partner for this helpful, in particular for clarity and a more complete summary. I find the writing of Anthropic models not bad, but I am happy for feedback.

I asked because it was posted by you but when I started reading it it didn't sound like you (or your previous work, datahike etc). It sounded like Claude.

this is amazing stuff!

@andersmurphy Fair enough, I wish I had more time to write myself right now, but the truth is that a lot of what I am doing is somewhat speculative work I thought about during my PhD, but could not execute on my own (it was just both cognitively [reading the details of all related implementations/papers] and physically [in terms of just typing] impossible). Now I can, so I try to get it out while I still have some time to do so and hope it will also help Clojure to demonstrate its value in new light, but nobody is paying for this, so for me the trade off is do I spend time writing or shipping. I want to find more time again to communicate it. The work is somewhat converging now around the compiler and dependent type + self-optimizing stack that is reflected in the different projects for #C09622F337D right now. If there is anything you want to talk about I am happy to reply here or in DMs.

Appreciate the honesty. I'm a huge fan of your work (datahike in particular but also the linter for datalog has saved me many times). But, I dismissed your latest stuff because though the ideas sounded interesting the communication was all Claude and I've been burnt repeatedly (in terms of wasting my time) interacting with projects that use claude to write their docs/comms (not to say you can't use LLMs to build impressive things, given enough discipline/structure), I've personally found when the comms are Claude I'm going to be wasting a lot of my time chasing ghosts in the machine. Anyway best of luck what you're building sounds very cool. 🔥

Thank you that is valuable, and I feared that this is the case as well, because I have also seen a lot of crappily written AI "slop" (I am somewhat careful with throwing catchwords around for such a complex phenomenon as emergent AI). I think you are right that I have to spend more time writing myself again probably, to make it more credible and also pay more attention to all the details. The goal for now is to establish the full vertical integration and libraries and then refine them. Wandler specifically is research software, because I also hope to get some feedback/ideas to make it fit better what Clojure devs need before sinking a lot of time in a fancy computational framework that will at best only ever be a conference paper or a personal toy.

Specifically if there is anything you need then I am happy to consider it and potentially integrate it.

If you don't have time to write about it yourself I honestly think you'd be better off waiting than try to cut corners with LLMs. I don't know what your goals are, but I've seen how you use LLMs and I now routinely ignore all of your work because of it. I have no idea if I can trust it in any capacity and the signals I have from how you present it do not convince me to go give it a go. All this to say: cutting corners with LLMs is undermining all the good work you did, at least for me.

Hello Sean! I have two questions: • Was it intentional that the fix hides in the misleading commit title "prep for 2.7.1389"? There is no link to the commit in the changelog either, for anybody to assess the risk and the fix https://github.com/seancorfield/honeysql/commit/efc698edc657c33c98eb60653554f4b250bd36e4 • Are there any examples of an actual injection done in this way? I see the tests check for the implementation of the fix but not for the injection itself, it seems.

See the thread in #C66EM8D5H about the undocumented interim releases while I was working with Younghun and others on testing two sets of fixes (2.7.1389 and 2.7.1390). Those releases have both been removed.

Those tests are indicative of how the CVE works: user input (or other arbitrary strings) passed into a program that simply calls keyword (or symbol) on those strings without sanitizing them, and passing them into various places in the HoneySQL DSL.

Would it be clearer if I lifted the bad strings out to a let and named them untrusted-input or something?

we had a researcher reach out to us about this as well.

Same researcher also reached out to James Reeves about Ring, which led to the 1.15.5 release.

Mr. Ko has been a busy little bee!

The reason I'm asking is because it is not clear to me why checking for suspicious characters is needed there at all, why such input doesn't go through prepared statements as everything else. Suspicious chars check doesn't feel like a holistic solution, more like a stop-gap heuristic

How would you make a prepared statement validate a part of the SQL string, not a parameter value? Or rather, not validate, but make it be passed through a prepared statement.

Prepared statements deal with parameter values in SQL. The potential injection vectors addressed in this release of HoneySQL are not parameters -- they are regular SQL syntax that cannot be turned into a parameter.

In the same way that you cannot have SELECT * FROM ? -- table names cannot be parameters, therefore HoneySQL must validate {:from (keyword table-name) ..} at the keyword/symbol level. Some vectors -- the most common ones -- were already checked in earlier releases. Mr. Ko found several new ones. The initial report was about this: {.. :order-by [:col (keyword dir)] ..} where dir could be passed an arbitrary string. After some back and forth, he detected other paths for injecting arbitrary SQL into a few other constructs.

Thank you for the explanation. It is still not entirely clear to me how vulnerable I might be, and if any of such usages are an antipattern in the first place. I will study more myself. > table names cannot be parameters Honestly, this was new to me, TIL. And that feels like a limitation.

If you are calling keyword or symbol directly in your code, to construct things to put into HoneySQL DSL expressions, you need to think about where the string comes from that goes into that keyword or symbol call. If you're just passing in strings, those will be lifted to parameters. That's a bit of a simplification but should be a useful guideline.