I've been thinking if this could be done in Nix and toyed around with the idea just a little bit using nano-gpt.
Hermeticity always seems to mean isolation, but depending on who you ask it does not always mean computing some sort of hash over all build input as the 'identity' of a particular step in the pipeline, like Nix does.
If you do that hash-based identity part, looking up intermediary results and resuming from there happens using this sort of hash.
Does savanah do that, or will it resume where it left off based on a less strict notion of identity?
A consequence of universal healthcare that people don't talk about much is that it turns unhealthy citizens from an individual cost into more of a collective one. So it makes sense that countries with universal healthcare regulate in favor of their citizens as opposed to their food industry, because they're paying for the consequences more directly.
I would blame how Austria, a very small country, is organized into 9 provinces that actually have their own budget and can pass their own laws on some topics.
Rail service is funded at the federal level, so there's less arguing about who pays for what. Bus service, however, is managed by regional transport associations funded by the provinces. This creates disincentives for cross-province bus routes because no single province wants to pay more than its 'fair' share for a service that primarily benefits voters in another province.
Similar dynamics play out at the city/province level. Take Linz, the provincial capital of Upper Austria: the city has had a social democratic (SPÖ) mayor continuously since 1945, while the province has had a conservative (ÖVP) governor for exactly the same period of 80 years. This disincentivizes the province government from helping to fund public transport within or into the city, because it's a win for social democratic city voters, while the more conservative rural voters would rather take the car anyway since they often can't do the whole trip by public transport.
Arguably the reason for the excellent public transport in the city of Vienna is that they are also their own province. Their mayor/governor, who has been a social democrat as well for the last 80 years, always controls both levels of funding.
If you make a conventional AI agent do packaging and configuration tasks, it has to do one imperative step after the other. While it can forget, it can't really undo the effects of what it already did.
If you purpose-build these tools to work with Nix, in the big picture view how these functional units of composition can affect each other is much more constrained.
At the same time within one unit of composition, you can iterate over a whole imperative multi-step process in one go, because you're always rerunning the whole step in a fresh sandbox.
LLMs and Nix work together really well in that way.
Yes, the cycle times are bad and some ecosystems and tasks are a real pain still.
I also agree with you when it comes to the task of auditing every line of Nix code that factors into a given system. Nix doesn't really make things easier there.
The benefit I'm seeing really comes from composition making it easier to share and direct auditing effort.
All of the tricky code that's hard to audit should be relied on and audited by lots of people, while as a result the actual recipe to put together some specific package or service should be easier to audit.
Additionally, I think looking at diffs that represent changes to the system vs reasoning about the effects of changes made through imperative commands that can affect arbitrary parts of the system has similar efficiency gains.
I think as AI gets smarter, defenders should start assembling systems how NixOS does it.
Defenders should not have to engage in an costly and error-prone search of truth about what's actually deployed.
Systems should be composed from building blocks, the security of which can be audited largely independently, verifiably linking all of the source code, patches etc to some form of hardware attestation of the running system.
I think having an accurate, auditable and updatable description of systems in the field like that would be a significant and necessary improvement for defenders.
I'm working on automating software packaging with Nix as one missing piece of the puzzle to make that approach more accessible:
https://github.com/mschwaig/vibenix
(I'm also looking for ways to get paid for working on that puzzle.)
I mentioned another alternative to adding flake-specific metadata to data structures that are transferred over the network, as part of the signed traces or otherwise, in a comment on that PR Eelco linked.
It's keeping flake-specific data locally, to guarantee that it matches how the user ended up with the data, not how the builder produced it. I think otherwise from the user POV such data could again look misleading.
As a current PhD student (working on Nix stuff) let me take this opportunity to congratulate you on your successful PhD defense and publicly thank you for your writing. That you write and what you write are inspiring.
I work with Nix a lot, and I had never seen `__findFile`.
It's kind of crazy how much there is to know about Nix. I wish there was a bit less surface area to the language. On the other hand it's really interesting how much specialized knowledge there is in the community around various topics. Some people package things, some people write library code, some write glue code that wraps other build tools, some write VM-based tests, some write generators that transform store paths into things like container images, some just manage their dot files, some are experts for how we deal with some specific proprietary ecosystem like cuda, some write infra code or tools around the Nix code, some work on one of the Nix implementations.
It saves you from escaping stuff inside of multiline-strings by using meaningful whitespace.
What I did not like about CCL so much that it leaves a bunch of stuff underspecified.
You can make lists and comments with it, but YOU have to decide how.
I wrote a paper about how I think trust should work for software dependencies.
It very much builds on the hash-based cache lookup mechanism this paper calls constructive traces (in contrast to what they call deep constructive traces) to eliminate transitive trust relationships.
I want to try to become an independent researcher, when the funding for my PhD position runs out.
My idea for financing this is finding a few companies who pay a retainer fee to not only get direct easy access to my expertise when they need it, but are also interested in the results of the kind of work I'm doing when they don't need anything specific from me.
I work on supply chain security with systems like Nix, and recently put up a first version of a website: https://groundry.org/
I know about mass rebuilds, but in the parent comment you were talking about fixed output derivations, and committing the hashes for a mass rebuild to version control is technically possible, but not a reasonable workflow, because it makes all changes that are mass rebuilds conflict.
What works better is keep track of those hashes as part of the signatures, which is already happening. There's a lot of interesting things that can be done with that kind of information, I'm one of the people working on that kind of stuff.
Basically I have a paper out about how verifiable and reproducible can come together like that in Nix:
You also couldn't feasibly do that for derivations that actually build packages, instead of fixed output derivations only, because if you the update the package set to include a newer version of the compiler, which would often produce a different output, in addition to having to rebuild everything, you would have to update all of the affected hashes.
What you should be able to do in the future with a system like nix plus a few changes is use nix as a common underlying mechanism for precisely describing build steps, and then use whatever policy you like to determine who you trust.
One policy can be about having an attestation for every build step, another one can be about two different builders being in agreement about the output of a specific build step.
That way you can construct a policy that expresses reproducibility, and reproducibility strengthens any other verification mechanism you have, because it makes it so that you can aggregate evidence from different sources.
and then have different build hosts
I think it would have been a good thing to mention, but difficult to do well in more than a quick reference or sidenote and could easily turn into a extensive detour. I'm saying this as someone who's working on exactly that topic.
There is a little bit of overlap between the kind of quantitative work that they do and this design aspect: the extensional model leaves the identity of direct dependencies not entirely certain.
In practice that means we don't know if they built direct dependencies from source or substituted them from cache.nixos.org, but this exact concern also applies to cache.nixos.org itself.
The intensional store makes the store shareable without also sharing trust relationships ('kind of trustless' in that sense), but only because it moves trust relationships out of the store, not because it gets rid of them. You still need to trust signatures which map an hash of inputs to a hash of the output, just like in the extensional model.
You can however get really powerful properties for supply chain security from the intensional store model (and a few extra things). You can read about that in this recent paper of mine: https://dl.acm.org/doi/10.1145/3689944.3696169. I'm still working on this stuff and trying to find ways to get that work funded (see https://groundry.org/).
Hermeticity always seems to mean isolation, but depending on who you ask it does not always mean computing some sort of hash over all build input as the 'identity' of a particular step in the pipeline, like Nix does.
If you do that hash-based identity part, looking up intermediary results and resuming from there happens using this sort of hash.
Does savanah do that, or will it resume where it left off based on a less strict notion of identity?
I could see arguments for either approach.