The Nix Thesis
The Purely Functional Software Deployment Model1 by Eelco Dolstra (herein referred to as "the thesis") is often pointed to as a great resource for learning about nix, albeit technical and formal. I wanted to read it myself, and see if it was as good as people said. I found that the thesis was very accessible, remarkably relevant given its age, and that a significant portion of the content was philosophical rather than technical. Therefore, my aspiration for this blog post is to crystallize some of the insights from the thesis into short form content. Hopefully this post will inspire you to go on and read the full text, or at least provide an expedient proxy for doing so.
I'm going to start at the end of the thesis. Dolstra, summarizing the thesis in the conclusion, says that the purpose of the project was to achieve a system for correct software deployment. He then goes on to explain that correctness is achieved through two main vehicles. First, through a precise naming scheme that leverages cryptographic hashes to concisely summarize the software identified by said name. This naming schema helps us achieve a much richer notion of equality than conventional naming schema (i.e. openssl-3.0.8). A "purely functional model" of software deployment. What exactly is meant by "purely functional model" is slightly unclear, but my understanding is that it boils down to immutable build artifacts, pure build processes (depend only on their inputs) that admit no side-effects, and compositionality of software components.2 The purely functional bit is particularly confusing because the nix expression language is itself purely functional, but the really critical piece is the functional principles applied to build and deployment strategies.
One ambiguity that might lead to confusion is that there is a distinction between the philosophical aspects of the thesis (i.e. an ontology of software deployment, and what constitutes correct software deployment), and the techniques / implementations that are guided by the theory. The Implementation Details section will try to explain how constructs (such as the cryptographic naming scheme, and purely functional deployment model) connect to the theory, albeit with less formality than the original thesis. The current section will look at the philosophy, and focusing on:
