Prompting agents to find optimization opportunities and bugs in Elixir codebases

The examples of both in the shape “Code: …, AI Finding: …, Fix: …” would have drastically improved the quality of this observation.

For me the real insight here is to force the agent to use Core Erlang, BEAM bytecode, Lean 4. Not in what form it reports the issues if you mean that.

I mean without an example this is not an insight. I was advocating for using static analysis with AI for more than a year already, but I am also an author of a bunch of static tools, way more powerful than just looking into bytecode, and I am an author of Cure language, making Lean4 just a redundant link in this chain.

That’s great, cause one of my goals were to learn more about this space. I’m now looking into Cure then.

What does formalising through Lean 4 gain you?

I admit I am no longer as worried about performance as I once was. Much more interested in idiomatic and easy-to-read code, not to mention self-explanatory and getting the job done in a minimalist manner (OK, now I am just repeating the same thing with synonyms).

I am not as far into the journey as some others but I found that formulating some property tests and doing a few (very expensive) mutation testing passes on key modules gets me in the territory of bug-free core business logic.

Not quite good enough but, since you mentioned the Pareto frontier, mine is: prove the code is doing what our spec requires, and try to minimise it and make it human-friendly. Barely any wins on the latter point still, admittedly. Currently gathering tools and libraries like Plyushkin and gradually am building my own ramshackle Rube-Goldberg contraption that hopefully will begin reducing coding lines in my professional work.

I can tell from my experience (that’s how I started Cure in the first place,) that in some applications (FinTech, Medical, Aircrafting, you name it) the cost of an error might be enough for the developer to want a proof rather than a “test coverage and probabilistic insurance.”

From a practical standpoint it finds issues with the code that I would not have found with simple prompting otherwise. So I can clone an Elixir codebase, tell my agent to try to formalize it in Lean 4 and interesting issues keep popping up through this approach.

I’m sure this is not the optimal way to approach this, it’s a new thing for me too. I will try to learn more about this since it already proved useful.

Sure, but I don’t know Lean 4. Any examples on how does it eliminate bugs, exactly? F.ex. compare against property tests? Sure enough, PBTs still rely on us to define, ahem, properties / laws, I wonder how much farther does Lean 4 go.

Oh, absolutely, but comparing deterministic techniques with LLMs outputs is a bit of a low bar. I am looking for a comparison of Lean 4 vs. other techniques (property / mutation tests), if you or @mudasobwa are willing to indulge.

Lean4 (or Cure on that matter) can prove that compiled code cannot get a reciprocal value for the currency exchange rate when crossing through several other currencies. No test can do that.

It can prove that the sum of two values cannot get a value beyond some interval. Etc.

There are people who think they can come up with tests covering all the corner cases and those who already know they cannot.

Alright, this is helpful.

But this bit in particular sounds like something we could do with PBTs today?

…provided we’re talking about calling a function or two, of course, and not fuzz CPU instructions and dig into the deep trenches where the Rust team spent years to make APIs for safe arithmetic operations.

Also, how easy it is to hook up to your own test suite, or is this something you periodically run, like a fuzzer?