[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.