I'm the author of this repository. I just want to point out that it was an experiment / proof-of-concept for the ideas of Girard's transcendental syntax (I didn

I'm the author of this repository. I just want to point out that it was an experiment / proof-of-concept for the ideas of Girard's transcendental syntax (I didn't even expect it would be posted somewhere outside of my small circle of collaborators -- that's why the "guide" is written in French). You could call it an "esoteric programming language" at this point if you want. I wanted to have fun while working on ideas I'm passionate about but also to build something people interested in Girard's works could play with. So it's not ready to convince anyone of its relevance yet. It wasn't even meant to be a programming language at first. Girard's ideas are indeed cryptic and may sound like a caricature of (a particularly grumpy) continental philosopher. One of my goals is to make these ideas more understandable and more down-to-earth, to show that they can be illustrated in a toy programming language. But there's a still a lot of work to be done (way more than what you could imagine just from reading Girard's papers). Although I studied Girard's last works for 4 years, I'm still far from understanding all its consequences. That's because it is related to pretty much everything in logic and computation (what is a type/formula/specification, how do you know whether an object is of some type, what is a proof, what is meaning, what is a system, what are logical rules, what all models of computation have in common, what all logical systems have in common, what is a program, what is an algorithm). The idea is to go beyond the current proof-as-program correspondence (on which proof assistants like Coq are based). After its analysis of the notion of proof, Girard wanted a computational space in which elements would be able to "test themselves", without relying on some "hard-coded" semantics. In programming terms, it would correspond to the ability to build types from programs. There is no primitive types, not even the arrow type of functional programming. We just have Prolog-like bricks of terms which can interact with each other. They can express programs or tests for programs. You build everything with that like how you do chemical experiments. To give a probably familiar illustration, I'm often asked whether we could "do transcendental syntax" with the untyped lambda-calculus. It would be possible if for any type T you could find a finite set of lambda-terms acting as "tests" such that interaction with it ensures being of type T. The space of lambda-terms is not "large enough / flexible" for that. You need to introduce exotic objects like how you extend the set of rationals Q to the real numbers R to solve more equations. You can also think of how to tell whether a finite automaton recognizes some (infinite) rational language without relying on an external semantics. You only have input words and infinite testing by feeding it all words of the language. But yet, we are able to do it with an external semantics. So the question is how you internalize semantics in the object language. If there's anyone who has any inspirations or insights, I'm open and interested. The right path to follow is still undefined. I just have some tools coming from my understanding of Girard's works.