> Sometimes you can prove mathematically that two different approaches are equivalent, but differ only in name or some parameter, and that's a unification of so

> Sometimes you can prove mathematically that two different approaches are equivalent, but differ only in name or some parameter, and that's a unification of sorts, without proliferation of standards. Certainly, but that would already be supposing most of the work to unify at the source level is done, unless an extremely strong normalization is possible. > Untyped lambda calculus (and its sibling combinatory logic) is just language for expressing logic, nothing more. And it already exists (arguably it's one of the first programming languages, predates Forth and Lisp by at least two decades) and is among the simplest ones we know. I actually became interested in LC so much recently because, believe it or not, expressing things in classical logic is often more complicated than expressing things in LC. (Personally, I prefer combinators slightly more) I don't deny the power of LC for some uses, but taking one program, reducing it down to an LC equivalent, and then resurfacing as another program (in a different language, but otherwise equivalent), or some other program transformations you may desire, would certainly be elegant in some sense, but very complex. It's like programming in Brainfuck; the language itself is very simple, and making mechanistic tooling for it is very simple, but I don't think the tooling we could invent in 50 years would be sufficient to make Brainfuck simple to read or write. Moreover, formalizations of, say, "button" are not a problem, but scaling to different screens, devices, use cases, and so on will greatly increase the scope. This OS represents input events this way, this hardware provides that sort of data. I think this is the same problem as to why people, everyday, don't bother to make formal arguments almost all of the time. It's not that a formal argument along the lines of "you didn't take out the trash today, so I have reason to be frustrated with you" can't be formulated or proven, but rather that the level of rigor is generally considered both fatiguing and unnecessary. Any time someone suggests something that should make things much simpler, I'm skeptical. There are things that have essential complexity too great to be made simple, and then humans maybe have an inherent overhead of accidental complexity, above and beyond the accidental complexity we accidentally add. I'm still interested to see where your efforts lead, but I'm not expecting to see cheap nuclear fusion for another 10 years at least, so.