The problem, of course, is that having only the one single "you can't win" law is severely underspecified, but the solution was too clever by half, and highlights the problem with this approach — every program will be under-specified, because, at some point, writing the laws becomes a bigger problem than writing the code itself.
This becomes a real issue because the combination of underspecified but rigid laws pushes the aI towards this sort of "creative" solution that matches the letter but not spirit of the law. In this case, the issue was obvious, but I seriously worry about what sort of shenanigans will occur in less obvious cases.
So, yes, that's the issue with laws: they only protect what you remember to write. They're not a silver bullet. But they can still be incredibly useful, because it takes a small law to protect against entire classes of bug, covering your entire codebase. For example:
LAW: "the sum of all balances in this contract must be zero"
This one liner would have prevented Ethereum's infamous "The DAO" hack, where millions were stolen and almost undermined the entire project. But if your laws are under-specifying or ill-specifying your intents, Bend can't do anything to protect you.
If you can find a law which the existing code obeys, and show it to a human, and if they agree, save it. And maybe the AI could make a decent guess as to what kind of laws would appeal to a human versus which wouldn't – a simple law identifying a fundamental constraint the system obeys is good, something really complicated or constraining something coincidentally true isn't
Or some kind of measure of coverage? you'd never want 100% – then your laws would become so complex you couldn't follow or maintain them – but if it is very low, that can be a signal to increase it
They are usually in the “tests” folder.
So anything capable of extracting unit tests is extracting “laws”.
One might consider the test name the text of a law. And the AI fills in the details.
But a good start could be found in the unit tests.
Unit tests check whether a specific code module is implemented correctly given its (implicit) specification.
Good “laws” are independent of the structure of the code.
Tests may be a useful source for inferring what the laws are, but much of the actual content of the tests aren’t “laws” at all.
if there are a dozen unit tests trying to determine if some regex can escape a sensitive area, then one can derive a generalized 'don't let the regex escape from here' type rule -- or at least you could theoretically. I'm sure in reality that'd be a big minefield much like harness self-skill-writing has been.
Imo LLM researchers would benefit a lot by reading what continental philosophers have said on the topic of language. Barthes, Sarte, Deluze, Derrida, et. Al have a lot to say that explains why we're running into the same problems over and over.
[0] https://www.commitstrip.com/en/2016/08/25/a-very-comprehensi...
I actually think Asimov is more instructive here, while Gödel and Tarski tell us the tool can’t prove itself…
Nonetheless, it is a worthwhile endeavor and I hope more rigorous practices like this catch on.
But that's how it is anyway, no?
Defining clear boundaries and clear goals is the hardest part. If you get those right everything else is rather trivial.
Respectfully I'm not sure if I share your worry though. You would have the same problem if you wrote extremely thorough / exhaustive unit tests or extremely precise types and didn't allow the LLM to amend them. You're basically shrinking the state space of what is considered a "correct" program per your spec. That the LLM has to get extremely creative to break your program is a _feature_; in my experience, an LLM does not have to get creative at all to break a typical program written in an enterprise setting, and that's unfortunate.
Of course because at its limit programming is basically defining desired behaviour under all circumstances and logical conditions.
I wonder if harness-hooks + Jev (equivalents) could semantically lint for `sloppy_law` etc when ever they are edited
Do you plan to invest in profile guided optimization or autotuning in Bend2 - using runtime profiles / cost models to make decisions around SIMD vs. multicore vs. GPU parallelization?
Bend2's model might give you a really nice view into available parallelization. Heck I can imagine integrating an LLM to profile and optimize in an absurdly expensive `-O7` optimization mode one day!
https://gist.github.com/VictorTaelin/77fd5a2a8a4a07e1da6157e...
> That same file is the CPU program and the GPU kernel: clang builds it for the host, Metal or CUDA builds it for the device, so a `!` runs the exact same code on either chip.
What exactly is this saying? The guide doesn't really explicitly define `!`, and it's unclear from this sentence whether it's saying that, "clang builds it for the host and Metal, and CUDA builds it for the device", or if it's saying, "clang builds it for the host, Metal, and CUDA, and builds it for the device", or something else entirely.
It just means that Bend compiles to a single .c file, and that file compiles to either Metal or CUDA, via macros, depending on your target. This shouldn't be relevant to most users. It is just a way I found to keep the file small and reuse as much code as possible, rather than rewriting the runtime 3 times (once for C, once for Metal, once for CUDA).
I'm confused - could you explain how the board/flag animation relates to Bend's compile time checking? Is it actually a direct demonstration of Bend running a check?
(Why it is done the way it is, what problems are solved by affinity, why closure can be called at most once, how a function that never returns can prove anything, and everything else)
If you mean about the type theory specifically, "Type Theory and Formal Proof by Nederpelt and Geuvers" is a good introduction. Not sure what I'd recommend on linear types, no book I know of is very introductory? Perhaps "Idris 2: Quantitative Type Theory in Practice", which is a language with similar foundations to Bend, and the author wrote a book on it (and inspired myself!)
É ótimo ver um brasileiro criando algo tão único!
You can find it on Bend's demo directory in our GitHub.
Don't tell anyone though!