[aftergibson]

As time goes on, I find myself increasingly worried about supply chain attacks—not from a “this could cost me my job” or “NixOS, CI/CD, Node, etc. are introducing new attack vectors” perspective, but from a more philosophical one.

The more I rely on, the more problems I’ll inevitably have to deal with.

I’m not thinking about anything particularly complex—just using things like VSCode, Emacs, Nix, Vim, Firefox, JavaScript, Node, and their endless plugins and dependencies already feels like a tangled mess.

Embarrassingly, this has been pushing me toward using paper and the simplest, dumbest tech possible—no extensions, no plugins—just to feel some sense of control or security. I know it’s not entirely rational, but I can’t shake this growing disillusionment with modern technology. There’s only so much complexity I can tolerate anymore.

[YouAreWRONGtoo]

Emacs itself is probably secure and you can easily audit every extension, but if you update every extension blindly via a nicely composable emacs Nix configuration, you would indeed have a problem.

I guess one could automate finding obvious exploits via LLMs and if the LLM finds something abort the update.

The right solution is to use Coq and just formally verify everything in your organization, which incidentally means throwing away 99.999% of software ever written.

[otabdeveloper4]

Formal verification solves nothing. You can have a formally verified 100% secure backdoor exploit. (Ultimately it all depends on the semantics of "sysadmin" vs "hacker", who are really just two different roles of the same person.)

This is also why signing code commits isn't a solution, only a way to trace ends when something fucks up.

[YouAreWRONGtoo]

Formal verification would solve everything. It's just that whoever is using the software actually needs to understand the specification, but when there is some trusted base of I/O primitives (like "read a file"), such things become trivial to check; even Haskell has such things in a limited fashion via SafeHaskell and to an even lesser extent via its IO monad.

The specification for a text editor would be much simpler than an implementation. For example, efficiently searching for a substring is non-trivial, but a specification is easy. So, all that I would be interested in, is a proof that "eval(optimized_substring_search needle haystack) = eval(easy_substring needle haystack)", for example. Obviously, there are many thousands of such theorems that would have to be done to clone Emacs, but at least a new release wouldn't contain bugs anymore (wrongly specifying something would happen, but it's much easier to write a specification of desired behavior than to find the exact bug in some mess from someone else, because it conflates implementation and specification in the first place).

[otabdeveloper4]

You completely, 100% misunderstood my comment.

[YouAreWRONGtoo]

I did understand; it's just that I am way ahead of you.

Your point is that users are too stupid/lazy to comprehend specifications. That is, they won't bother to read that the specification of their formally verified secure version of Google Maps really just copies their credit card data to a random server.

I just don't agree.