I basically want to get to a point where computer science becomes indistinguishable from mathematics. So that we would get rid of talking in terms of “web servers”, “immutable event logs”, “relational databases” etc. etc. and would instead only use terms from category theory and mathematics in general, therefore achieving maximum composability, reusability and eliminating all duplication of logic. I also asked the AI “research very deeply for the top-notch canonical approaches to model a von Neumann computer in category theory” yesterday and (not sure yet how much sense it makes, I’m just learning all this autodidactically) I got “the Lawvere theory of global state for memory, the Elgot/Conway dagger for the control loop, traced monoidal categories with delay for the clocked datapath, Turing objects for “programs are data”, and polynomial coalgebras for the machine as an interactive system.”
Architecturally, firstly let’s assume each of us would have our own server and we can send any data between each other. Now let’s say you define a cool function f and I want to use that function on my server too. In the most basic case, it might be a pure function, say f(x)=x+3, with x being an integer. But what if it interacts with the real world?
I think the most important part of my research question (see https://www.nalenz.org/ and https://research.nalenz.org/) is the part “without requiring everyone to agree on one universal representation of reality”. So I do _not_ want to say “everyone must use this language” (https://xkcd.com/927/) or “everyone must use this logical framework”. Instead, when your server would send your cool function f to my server, firstly it would unwrap it from some serialization format (maybe JSON, XML, Protobuf etc.) and then in the metadata it would say which “doctrine”/theory/logical framework it adheres to, so that when my server receives it, it can ingest it, apply the morphism from f’s theory to the theory it uses internally and then start the execution. For example for f(x)=x+3, it should not depend on the _encoding_ of that function, but instead the _structure_ “natural numbers with zero and successor”. Besides Dedukti, I had also found https://uniformal.github.io/, which also claims to “integrate the 4 major paradigms for representing scientific knowledge”. Then there is also http://hets.eu/ focused on logic translation and this idea of “institutions”, but seemingly also more for proofs instead of for actually executable logic.
Then I kept going and now it seems like the architecture would be “ship terms of a theory, not code, and let the receiver supply the model”. So for example “Natural numbers with zero and successor” is a theory T. Then when my server implements a model of T, there’s a unique homomorphism from the initial model into mine, so f means exactly one thing on my machine. And for real-world interactions, my server runs them by providing a handler, which is a model of that algebraic effect theory in my own world. Seems like https://koka-lang.github.io is based on that idea. And then there is https://openmath.org/ which claims to be “an extensible standard for representing the semantics of mathematical objects” and its “SCSCP (Symbolic Computation Software Composability Protocol)” (https://openmath.org/standard/scscp/) which again _sounds_ nice, but no idea how much substance is behind it. Then I also found “choreographical programming” which seems to be more for distributed systems, which is also so important I think to get right, because the collaborative aspect of this system so important to me.
Then I found “call-by-push-value (Levy’s calculus)” (https://en.wikipedia.org/wiki/Call-by-push-value and https://pblevy.github.io/papers/thesisqmwphd.pdf) which seems to also be a whole new paradigm for such an intermediate language. I didn’t even know the difference between CBN and CBV before, but apparently: “Category theory introductions, logical frameworks (Dedukti, MMT/UniFormal, Hets) and OpenMath all mostly deal with pure, terminating terms. There, evaluation order doesn’t matter: CBV and CBN give the same answer, so those communities rarely mention it. The distinction only becomes important once you have effects or non-termination. For example, print(”a”) + print(”b”) behaves differently depending on when and whether arguments run. That’s exactly where your question went with “what if it interacts with the real world?” So this isn’t a gap in your existing research, but you’ve reached the point where the logic side and the programming language side meet, and CBV/CBN is the first thing you find there.” The part “CBPV remains a unifying starting point in the study of computational and logical phenomena” from https://siglog.org/winner-of-the-2025-alonzo-church-award/ also sounds quite interesting. Unfortunately here the software side seems still quite thin, only PoCs like https://github.com/zydeco-lang/zydeco
So I guess my main curiosity is: Would Dedukti have any place as an “intermediate representation” in this stack, for example splitting it so that logic stays in Dedukti and effects become CBPV? Also, does any interoperability between Dedukti and CBPV (potentially a “λΠ-modulo signature” for CBPV?) already exist? And then my more general curiosity is not specific to Dedukti or LambdaPi, but instead I feel quite stuck in analysis paralysis and just really want to _get started_ with _some_ way to translate all the stuff I’ve already written in traditional programming languages (mostly TypeScript) into some representation (”theory”?) that is independent from the language itself, so that I can then create something like a compiler/interpreter for it as the first reference implementation and eventually something like Wikifunctions to make it distributed and collaborative. I just want to feel secure in the choice of language I make for this “intermediate representation” as well as my first reference implementation, so that I won’t have issues in the future around composability, provability, error handling, making it distributed, real-world effects, reactivity and making it processor-independent (WebAssembly?).