I have a solution based on Nix that can be used to generate reproducible container images: https://github.com/nothingnesses/agent-images . It lets you customise which agents, harnesses, or any other packages you want included in the VM and it uses `agent-box` for sandboxing.
I've been thinking a lot about this recently. In my case: how do I get an agent to see the important parts of the current plan and get it to stick to it without deviating, especially as loops get into longer and longer cycles and compactions erase prior context?
I think the problem with just encoding a whole plan in a single markdown file is that it gets polluted really quickly (agents can stop adhering to instructions to keep it clean and conform to a specific structure), which makes it harder for agents to see which parts of the plan they should focus on. As such, I've reached a similar conclusion about giving the agent access to CLI tools to help them deal with this. To try to mitigate this, I've been getting Claude to develop for me a CLI tool that:
1. Scaffolds reusable, structured plan templates and a reusable workflow that structures how to tackle the plan, step by step.
2. Validates that the plan files still conform to the correct, parseable structure.
3. Parses and evaluates the plan files, to determine what the current state is and what the next valid transitions and states are according to the workflow, like a state machine, and outputs instructions and reminders for agents as to what they should do at each step of the workflow.
So far, I've been dogfooding the tool and it seems promising: I can leave Claude running for longer and it doesn't drift as much. However I haven't ran any benchmarks yet and I'm still not entirely happy with the state of the codebase ( https://github.com/nothingnesses/agent-scaffold ), so take this with a grain of salt.
That said, I'm also bullish on using agents with formal methods and proofs. Type checkers and compile-time checking in general are great because they surface errors early and with great specificity. So if you can encode your specifications with, e.g. dependent types, you can use the type-checker as a way to steer the agent when it goes wrong and gets off-track.
I've codified mine into a reusable workflow https://github.com/nothingnesses/agent-scaffold . To be honest, this isn't fool-proof though, since the agents can simply choose to ignore them, so I also like to pair this with deterministic linting and compile time checking.
For a Rust project, I created macros that output compiler errors when documentation and tests are not in a shape I want them to be, like missing function invocations or assertions, which forces the agent to address them, where otherwise they would've just worked around them by adding stupid trivial assertions like `assert_eq!(true, true)`.
That still isn't fool-proof either, but it helps minimise those instances. I'm bullish on the idea of integrating formal methods and model-checking with AI. I think that combo feels like a promising avenue for constraining the stochastic side of AI-generated code with something closer to deterministic verification. Provided you can write correct specs of course!
I've contributed to https://github.com/0xferrous/agent-box which allows you to bind-mount git repositories into containers that agents operate in, preventing the agents from accessing files that aren't bind-mounted. Your usual .gitignore can then be used to also ignore files within the repo to be bind-mounted, which prevents agents from accessing them at all, essentially working as a sandbox.
I also maintain https://github.com/nothingnesses/agent-images which allows you to use Nix to reproducibly spin up OCI container images containing agents and any other tools you need for development and use these with agent-box.
I use both at the moment to work on some personal projects with agents, where I set up multiple separate git worktrees for the agents to work in, preventing them from accessing anything outside of the worktrees and from trampling over each other's work.
In case anyone is interested, I'm also using bash scripts to run my agents in containers. It's simple, but has only bash and docker as dependency: https://github.com/asfaload/agents_container
I've contributed to https://github.com/0xferrous/agent-box which allows you to bind-mount git repositories into containers that agents operate in, preventing the agents from accessing files that aren't bind-mounted. Your usual .gitignore can then be used to also ignore files within the repo to be bind-mounted, which prevents agents from accessing them at all, essentially working as a sandbox.
I also maintain https://github.com/nothingnesses/agent-images which allows you to use Nix to reproducibly spin up OCI containers containing agents and any other tools you need and use these with agent-box.
I use both at the moment to work on some personal projects with agents, where I set up multiple separate git worktrees for the agents to work in, preventing them from accessing anything outside of the worktrees and from trampling over each other's work.
Out of curiosity, what do you think is wrong with monomorphization-based polymorphism? The other alternatives I'm aware of are 1. type-erasure via v-table based dynamic dispatch (which Rust also has in the form of the `dyn` keyword), which has performance and memory-allocation overhead and 2. macros, which Rust also has and, if used for polymorphism, would essentially be like compile-time monomorphization, but clunkier.
Maybe I'm missing something though and there are other alternatives done differently in other languages?
The correct choice IMHO is type-erasure. It does not necessarily have overhead, because optimizers can specialize or devirtualize. Of course, this my depend on how you implement your language, but in C this works nicely. The problem with monomorphization is that it leads to exponential expansion, which later passes of the compiler can not unify again (at least this is much harder than not expanding in the first place). It should also fundamentally limit what you can do, because expansion has to stop at some point, but I haven't thought about this too much.
I also think that where you want monomophization, macro seem fine. I do not think this necessarily has to be clunky, but this is just a guess.
Type-erasure does have an inherent overhead. Sure, optimizations can be made, but they can be fickle and specialization is basically implicit monomorphization.
Using C macros to replicate Rust's monomorphism has several drawbacks: they are inherently unhygienic, even in comparison to Rust's own; you can't set type-bounds; they aren't even a part of C proper, etc.
I prefer Rust's approach with the choice between generics, macros, dyn and Any.
What inherent overhead does type-erasure have? The optimizer can always specialize just like for monomorphization. The difference is that it does not have to do this. Monomorphization specializes everything before the optimizer even has a chance to look the the code. So it fundamentally can not have advantages, only restrictions.
C macros are certainly a proper part of C and one can also certainly add type-bounds. But yes, they are not ideal. Still, if one wanted to do this, one could certainly improve them a lot for type-generic programming. I would prefer this to having macros, generics, a const expression sublanguage, and vtables.
The inherent overhead of type-erasure is the vtable. Which is funny, because you said you prefer one over the other at the end, when they are basically synonymous. The compiler may choose to devirtualize and specialize, but that isn't guaranteed. If you want this behavior, &dyn does the exact same thing.
Specialization provides more opportunities for optimizations, whereas proper type-erasure (which bars specialization optimizations) doesn't due to lack of type information.
"C macros" are a part of the preprocessor, which runs before the actual C compiler. As such, it lacks all semantical information the C compiler would have at that point, such as function implementions. In practice, macros in C serve two purposes: manipulating C source code (which Rust macros can also do, but with more hygiene); specialization polymorphism, but worse (in which both Rust's generics and C++ templates do better).
The vtable can be removed in all cases where you specialize by monomorphization, so the overhead compared to it is not really inherent.
Type-erasure can be undone by specialization. In contrast, monomorphization specializes the code first, at which point it becomes much more difficult to unify it again.
Sorry, my comment about preference was badly phrased: What I meant is that I prefer to make macros better, than having all the different but partially overlapping techniques in the same language. This is the complexity I am complaining about in both C++ and Rust.
As I stated in my follow up, vtables can only be removed when the type information is still available, which, generally, aligns with specialization, except when dealing with libraries (even with LTO). You say the "vtable can be removed in all cases of monorphization", but that isn't guaranteed and often requires double guessing the compiler to ensure it still knows the type, where as monorphization makes it explicit when the compiler doesn't know the type anymore and that specialization must occur.
The problem with your suggestion about macros is that it misunderstands the reason why different techniques exist. While they may overlap, they have different primary niches: Rust macros provide codegen and inline DSL, Rust generics/C++ templates provide monomorphism, C++ constexpr/Rust const fn evaluate expressions in compile time, etc.
Extending preprocessor macros, aside from requiring integration into the C language proper, would likely create something much more complex and with poor DX. Specially so if it tries to fulfill all niches, as each of them often operate at different abstraction levels, with different ergonomic requirements that are often at odds with each other.
I just noticed you said "The compiler can always specialize". That's indisputably false. That only happens if the compiler has enough information to infer the concrete type at the call point. Conditionals, collections, or anything that may throw doubt about original type info and their function implementations can (and normally will) disable specialization.
Not necessarily. In pure theory, yes. But in pure theory, monomorphized code can be deduplicated too.
Monomorphization often forces types information to flow, whereas type-erasure considers that a bonus. As such, a compiler may accidentally introduce opaque boundaries that hide type information. Even in cases where this is the programmer's fault and the type info is truly lost, in monomorphisation, that becomes an explicit error, while, for devirtualization, since it's just an optimization, the call is silently revirtualized (until someone notices it while profiling/decompiling). One has explicit intent, the other doesn't.
The point is much easier to propagate information (and not accidentally lose it) than to deduplicate after specialiation, so I do not agree that this is only of theoretical relevance.
I agree that monomorphization has explicit rules that force specialization, I do not think this is an advantage at all because it is too rigid and one can introduce explicitness at the language level also for devirtualization where this is needed. In this sense, monomorphization is premature optimization which limits what can be expressed at the language level and makes the job of the optimizer much harder (and practically impossible to undo the damage completely).
You seem to be underestimating how easy it is to lose type information. Creating a array of type-erased is already enough to cause confusion, even if the surrounding code is enough to prove the array only has one type. If we are to assume perfect deductive ability for type-erasure, why not for monomorphism as well?
Monomorphization isn't premature optimizations either. It and type-erasure are semantically different. For instance, only monorphization can enable inlining of data structures (as devirtualizating an array of fat pointers involves dealing with ownership concerns, among other things). You either have to type-erase the array itself or box all the items, none of which are very ergonomic for a system-level programming. Also, in terms of performance, monomorphization generally makes the compiler's job easier overall in comparison to type-erasure (specially in Rust where types also encode lifetime), so I don't see the damage unless you are dealing with an extremely size-constrained environment or dealing with instruction cache misses (which is an indication of poor abstractions).
Finally, as stated elsewhere, it's trivial to implement any type-erasure polymorphism in a monomorphic system (save for very specific exceptions, related to hardware), but the reverse is not true. To do so reliably will require assistance of an external codegen tool, like the C macros, generally recreating monomorphism, but worse, as the compiler doesn't actually know the polymorphic code is related, making deduplication even harder.
I don't see why it would easy to lose type information in circumstances where you can do monomorphization. Note that I do not assume "perfect deductive ability". The practical observation is simply that it is far more effort to deduplicate than to clone.
From the code, we can already tell all elements have the same type, but the compiler is already adding checks. One of the options would be to convert the array of fat pointers into a fat slice. But now you have to enlarge the slice's vtable with all possible item operations, even if we don't use them often. Alternatively, use monomorphism. Or use both.
I see, this is what you meant. GCC can not currently do this. But this also not something that would correspond to a monomorphic version. A polymorphic function over a generic array would be specialized to one member type via monomorphization. This would correspond to this: https://godbolt.org/z/nd333xeTP
Aside from being heavily optimization-dependant, thinking through this, I've realized that type-erasure is a bit of a premature abstraction. It forces programmers to use indirection and pass-by-reference/pointer. It forces functions to be type size and alignment-agnostic. That's why type-erasure can't express monomorphism proper, whereas the reverse is not true.
It is trivial to see that the compiler could do inlining also in this case. Your modification does not "break" inlining in the sense of making it impossible. In fact, just making the vtables "const" is enough and it does it: https://godbolt.org/z/oYv47xx8G Or adding "inline" would also do it. (But this not why your argument is wrong.)
The compiler chooses to not inline in your example. And this is the point: The compiler makes inlining decisions based on some heuristics exactly because inlining is not always an advantage (even if it is in toy examples), otherwise it would do it far more often. Implementing type-erasure gives it the freedom to do this while monomorphization hardcodes it. It takes away this freedom. You can get the same result as monomorphization by forcing certain inlining or function-cloning decisions, but the reverse is much harder: you can not automatically deduplicate the already expanded function. (in theory yes, in practice no)
The argument that for a language with type-erasure the inlining heuristics of this specific C compiler may not be ideal, is rather irrelevant. (but interprocedural value propagation is rather smart in principle)
My issue isn't that the modification made it impossible to inline, more so how trivial it was: I just added a different type. Generally, optimizations are disabled not because the compiler finds them inneficent, but because it lacks enough contextual information/intelligence to safely add it. So similar to what you said, in theory, the compiler can optimize type-erasure just like monomorphism, but, in practice, it lacks info to do so. Either by programmer accident, language/compiler limitations, or both.
Also, monomorphization doesn't actually take the compiler freedom away (on its own) to optimize. Similar to how type-erasure can be optimized to behave like monomorphization through devirtualization, monomorphized calls can be virtualized (which Swift shows). The problem is that it takes away transparency from the programmer. It also changes the semantics of the call behind the scene (type-erasure is strictly pass-by-pointers, monomorphism is not). That wouldn't work well for a low-level language.
But your example did not show that the compiler lacks the contextual information. My argument is exactly that in all cases where one can do monomorphization, this contextual information is trivially available because it simply a small part of what can be done with interprocedural constant-propagation anyhow. I think this is easy to see.
I am not commenting on your Gish Gallop of new arguments.
How did it not lack of contextual info? By adding "const", you provided more info to the compiler, and it decided it was safe to inline, despite no actual behavior change. My point is, despite the possibility, these optimizations are easy to disable by mistake.
Also, there's no gish-gallop. You said the compiler can optimize type-erasure like monomorphization, but not monomorphization like type-erasure, and I said that's not true: the compiler can, in fact, do that. I simply addressed your argument. The rest simply elaborates on why languages why might not do it.
No, you did not address my argument. You need to show that it is impossible (or hard) to do function cloning when using interprocedural constant-propagation in a situation where monomorphism does this. But nothing you said contradicts this and the fact that a C compiler may sometimes decide to inline or not a function is completely irrelevant to this question.
In fact, it was exactly my argument that it is an advantage of type-erasure that the compiler has more freedom. An example where the compiler does not specialize a function just demonstrates this flexibility.
I feel like you are attacking a strawman here. My point isn't that it's impossible to optimize, but such optimizations are fickle and easy to break by programmer error and require adequate language expressivity (although low-level languages generally provide that).
You say that the compiler made the decision to not inline it because it judged it to be the most efficient, yet, by adding the "const", thus adding more info, it did inline it. Why did the heuristics change here, even though the logic remained the same? I argue it's not because the compiler decided it would be more performant to not inline, but that it was acting on the side of caution.
Finally, if giving the compiler more freedom to make choices is your goal, then forcing it to start by either type-erasure or monomorphization is the wrong answer. The compiler should be free to choose type-erasure/monomorphization from the start in such case. However, that introduces limitations to the language. Since the generic function is prohibited from knowing the type size at compile time, it can't allocate space for it in the stack. Long story short, I think you'd be forcing the programmer into an abstraction they might not need nor would necessarily help them, and then hoping the compiler to optimize appropriately.
Personally, I care about expressivity and transparency, thus I think having both natively supported is preferable. But if one must be chosen over the other, monomorphism should come first, as you can build a vtable with it (also, there are many ways to build vtables and dynamically diapatch).
Not sure what numbers you are talking about. If you use qsort from the C library the comparison function will not be inlined, but if you provide your own, this is no problem.
If just "providing my own" would help why wouldn't the stdlib benefit too? You're going to have to spell out what you think can actually work here if you want me to believe there's "no problem".
It would also, but nobody cares enough because qsort is already fast enough for most things, and if you cared it is simply enough to do yourself. Are you doubting that C compilers can devirtualize function calls? Here is a small example that illustrates this. The compiler dervirtualizes all calls than folds the result: https://godbolt.org/z/E6cMMr8vx
How does this compare to https://academy.fpblock.com/blog/quickcheck-hedgehog-validit... ? As far as I understand, Validity also has free generators and shrinking for types by having them implement various typeclasses that represent invariants and also has pre-made combinators to test properties with.
So with the caveat that I'm not super familiar with Validity...
The biggest thing that leaps out at me looking at it is that Hegel is very built around flexible user-specified data generation (using the library's base generators and combinators) mixed freely with test execution. Validity in contrast looks extremely type-based, which is convenient when you're only testing fairly general properties of built-in types, but I've never found flexible enough to be a really good basis for property-based testing once your testing needs get even a bit more complicated. e.g. a lot of tests want some sort of upper and lower bounds on their numbers, and I don't want to define a type for each.
For an only slightly more involved example of this, suppose you've got, say, a Project type, and Projects have an owner that is a User. You might want a test that is about a single user that has some number of projects. In a generator-based approach, this is easy: You just generate a User object, then you generate a bunch of Project objects that have to have that User as their owner. Just works.
In contrast, in a type based approach, there's basically no way to express this without e.g. defining a new ProjectsOwnedByASingleUser type and defining what it means to be a valid instance of that type... It's a lot of machinery for what is IMO a strictly worse user experience.
Git is so established now that it's sensible for alternative VCS to have a mode where they can imitate the Git protocol - or seven without that you can still checkout the latest version of your repo and git push that on a periodic basis.
Git is not a protocol, it is a data format. That only makes sense when your VCS system is similar enough to git to easily allow converting between the two representations.
It solves problems that you dont encounter if you are asking that question. I’ve lost a literal year or more of my life, in aggregate, to rebasing changes against upstream that could have been handled automatically by a sufficiently smart VCS.
An alternative explanation is that I already have a tool that helps me with these situations. The question was a bit rhetorical, because the vast majority of devs don't care what language many of their tools are written in or what algos are used.
A different example, Go's MVS algo can be considered much better for dependency management. What are your thoughts on the SAT solver being replaced in your preferred language tooling? It would mean the end of lock files
```
for HASH in $(cat all_changes.txt); do
pijul apply "$HASH"
pijul reset # sync working copy to channel state
git add -A
git commit -m "pijul change: $HASH"
done
```
git remote add origin git@github.com:you/pijul-mirror.git
git push -u origin main
