Hacker News Reader

Comment by pcwelder | Hacker News Reader

> 3. The "Trust but verify" pattern

To add on to this point, there's a huge role of validation tools in the workflow.

If AI written rust code compiles and the test cases pass, it's a huge positive signal for me, because of how strict rust compiler is.

One example I can share is

https://github.com/rusiaaman/color-parser-py

which is a python binding of rust's csscolorparser created by Claude without me touching editor or terminal. I haven't reviewed the code yet, I just ensured that test cases really passed (on github actions), installed the package and started using it directly.

View on HN

I checked the code. The code validates that values are within the range https://github.com/rusiaaman/color-parser-py/blob/ec739c80ba... but the library it wraps already does validation and a lot more checks (see range check here: https://docs.rs/csscolorparser/latest/src/csscolorparser/par...). So the code generated by AI has unnecessary checks that will never be visited.

You might look into why rgba_255 return a fixed-length tuple while rgba_float returns a fixed-length list.

If it's so important to test isinstance(r, int) then you should also have tests for g and b, and likely similar tests for the floats.

Is is really worthwhile to 'Convert back to ints and compare' when you know the expected rgba floats already?

The readme even confuses itself, as the example shows rgba_255 returning a list and not a tuple. Oh well, I guess Claude was confused by the conventions between Rust and Python.

Also, all the checks of "if u8 < 255" will make me not want to use this library with a 10-foot pole. It screams "ai" or "I don't know what I'm doing" so much.

First one is due to me asking it to return a 4 tuple instead of a list for the rgba_255 specifically, I guess it didn't update Readme or other return values.

The second is an artefact of a test case failing, which it tried to fix it using this check. Thankfully not a correctness failure, only optimisation issue.

You're right though it's not worth publishing for general public.

Well this is a good experiment. I don't find your idea bad at all: use AI to autogenerate bindings to expose a library in another language. This would be a good usecase for AI as it's not complex (well, most of the times) and is a lot of boilerplate.

Publishing the repo is worth it, because it showcases what the AI can (and cannot) do, and it is not there yet. But as a real package to pypy, indeed less.

What gets me is that tools like SWIG exist, in that case a tool which started in the 1990s to read a C header file and autogenerate bindings for Python and other languages.

Or, JPype uses reflection to generate run-time bindings from Python to Java.

Why does it require AI and all of this infrastructure?

For the same reason people use AI for some coding tasks: it generates boilerplate without needing to be programmed by an human. SWIG needs to be adapted to every language, and only targets C libraries. What about Rust, like in this case?

This is a case where LLMs can be good, because they can infer quite a bit about the needed scaffolding, and can generate bindings between languages where no such tool exist. We don't need to write a tool for every combination of languages (or adapt one like SWIG to add a language).

But in the long run, depending on how many bindings we need, the cost of each binding may end up outweighing the upfront cost of a human writing the tool.

> What about Rust, like in this case?

I didn't explain myself well enough then. In the specific case of Rust, why doesn't Rust already have a way to tell tools what the API is, and why aren't there already tools which convert that API to bindings for other languages?

Ideally, "import rust_ffi; color_lib = rust_ffi.load_library('csscolorparser')"

We already saw from pcwelder's other responses that this AI generation required human involvement ("me asking it to return a 4 tuple instead of a list").

We can also see style questions, like how is_valid is a static method on the ColorParser class, rather than a module-level function as I would have done, so the API intrinsically cannot be automated.

Which I knew from my own experience in developing Python bindings to C libraries. If you want it to feel like Python, rather than C, you will have to put in the work. (In my case, to add class structure, to hook into Python's garbage collection, to match the iterator protocol, and so on.)

Did you write the test cases?

TDD is, in my opinion and based on some tentative forays, one of the areas where LLM assisted coding really shines.

No everything in the repo is AI generated.

Them you really have no idea what you are running. Why include test cases at all?

How can you trust the tests? Sure, they may pass, but they could be testing for the incorrect outcome.

I've been saying for a while that formal verification seems like the obvious way forward here. Test cases are good but only cover a limited number of cases, whereas formal verification can cover all cases.

The biggest reason that we don't see formal verification being used more is that it takes some time to formally define the output of an algorithm and significantly more time to convince a theorem prover that your code is correct according to the pre- and post-conditions. If we can get LLMs to work well alongside formal verification tools then I think that would greatly improve their usefulness.

Here's a made up and trivial example of how I imagine this might look:

User: Write me a binary search over "type A_Type is array (Integer range <>) of Integer;"

LLM: Implementing the following:

    function Search (A : A_Type; Target : Integer) return Integer with Pre => Sorted (A) and Target in A, Post => A(Search'Result) = Target;

    First implementation:

    function Search (A : A_Type; Target : Integer) return Integer is
       Left : Integer := A'First;
       Right : Integer := A'Last;
    begin
       while Left <= Right loop
          declare
             Mid : Integer := (Left + Right) / 2;
          begin
             if A (Mid) = Target then
                return Mid;
             elsif A (Mid) < Target then
                Left := Mid + 1;
             elsif A (Mid) > Target then
                Right := Mid - 1;
             end if;
          end;
       end loop;
    end Search;

Compiler:

    Phase 1 of 2: generation of Global contracts ...
    Phase 2 of 2: flow analysis and proof ...
    
    wrapper.adb:12:36: medium: overflow check might fail, cannot prove lower bound for Left + Right
       12 |            Mid : Integer := (Left + Right) / 2;
          |                             ~~~~~~^~~~~~~~
      reason for check: result of addition must fit in a 32-bits machine integer
    wrapper.adb:12:45: info: division check proved
    
    wrapper.adb:14:19: medium: array index check might fail
       14 |            if A (Mid) = Target then
          |                  ^~~
      reason for check: value must be a valid index into the array

LLM: Looks like there's a possible overflow for very large arrays, attempting new solution...

Etc. until a valid solution is found and the result is returned to the user.

As an aside, this bug was present in Java for 9 years and would have been caught by formal verification (which admittedly was more difficult at the time): https://research.google/blog/extra-extra-read-all-about-it-n...

The use of formal methods has historically been limited to very limited niche areas. The volume of code that is covered by formal verification is some ridiculously small percentage of the overall amount of code out there.

The reason is probably that it is too tedious/difficult and you need some rare skills to do it. And mostly the categories of bugs it eliminates are not problematic enough. Either way, the amount of people capable of writing code vastly outnumber the people capable of formally verifying that code. I know a lot of programmers without computer science backgrounds that definitely have never been exposed to any of this. I have been exposed to some of this. But that's 25 years ago. And the persons teaching me that lived out his career in academia without ever working on real code that mattered. A lot of this stuff is rather academic and esoteric.

Of course, LLMs could change this a quite a bit. A lot of programming languages are optimized for humans. Lots of programmers prefer languages that sacrifice correctness for flexibility. E.g. static typing is the simplest form of adding some formal verification to a language and a lot of scripting languages get rid of that because the verification step (aka. compilation) is somewhat tedious and so is having to spell out your intentions. Python is a good example of a language that appeals to people without a lot of formal training in programming. And some languages go the other way and are harder to use and learn because they are more strict. Rust is a good example of that. Great language. But not necessarily easy to learn.

With LLMs, I don't actually need to learn a lot of Rust in order to produce working Rust programs. I just need to be able to understand it at a high level. And I can use the LLM to explain things to me when I don't. Likewise, I imagine I could get an LLM to write detailed specifications for whatever verifiers there are and even make helpful suggestions about which ones to pick. It's not that different from documenting code or writing tests for code. Which are two things I definitely use LLMs for these days.

The point here is that LLMs could compensate for a lack of trained people that can produce formal specifications and produce larger volumes of such specifications. There's probably a lot of value in giving some existing code that treatment. The flip side here is that it's still work and it's competing with other things that people could spend time on.

That Java issue you mentioned is an example of something that wasn't noticed for 9 years; probably because it wasn't that big of a problem. The value of the fix was lowish and so is the value of preventing the problem. A lot of bugs are like that.

Formalism starts with intent and then removing ambiguity from that intent. Having intent is easy, removing it is not. Especially when you do not know the limitation of what you're using to materialize that intent.

Python is easy because it lets you get somewhere because the inputs will roughly be the set of acceptable inputs, so the output will be as expected, and you can tweak as things go (much faster for scripting tasks). But when you need a correct program that needs to satisfies some guaranteed, then this strategy no longer cuts it, and suddenly you need a lot more knowledge.

I don't think LLM would cut it, because it doesn't understand ambiguity and how to chisel it away so only the most essential understanding remains.