engboris · engboris · Oct 2, 2025 · Oct 1, 2025 · Oct 1, 2025 · Oct 1, 2025
diff --git a/README.md b/README.md
@@ -1,78 +1,95 @@
 # Stellogen
 
-**Note: this project is an experimental proof of concept, not a fully
-designed or specified programming language. It is better understood as a
-research project or an esoteric language.**
+Stellogen is an experimental, "logic agnostic" language that asks: what if
+programs and their meaning were built from the same raw material, term
+unification, without types or logic imposed from above?
 
 Stellogen is a *logic-agnostic* programming language based on term unification.
 It has been designed from concepts of Girard's transcendental syntax.
 
+Stellogen explores a different way of thinking about programming languages:
+instead of relying on primitive types or fixed logical rules, it is built on
+the simple principle of term unification. The goal is not to replace existing
+languages, but to test how far this idea can be pushed and what new programming
+paradigms might emerge from it.
+
+**For the moment, it is an experimental proof of concept, not a fully
+designed or specified programming language. It is better understood as a
+research project or an esoteric language.**
+
+## Philosophy
+
+Programs exist to solve needs, but they don’t always behave as expected. To
+reduce this gap, we use a separate formal language of types. Types act like
+**questions** we can ask, and programs act as **answers**.
+
+This language of types is powerful, but it also shapes and constrains the way
+we design programs. It defines which questions are even possible to ask. Typed
+functional languages, dependent types, and other formal systems provide
+remarkable guarantees, but they also impose a logic you must follow, even when
+you might prefer to proceed more directly, or even outside of such a system.
+
+Stellogen takes another path. It offers elementary interactive building blocks
+where both computation and meaning live in the same language. In this setting,
+compilers and interpreters no longer carry semantic authority: their role is
+only to check that blocks connect. The semantic power (and the responsibility
+that comes with it) belongs entirely to the user.
+
 ## Key characteristics
 
-- **typable** but without primitive types nor type systems
-- both computation and typing are based on basic **term unification** between
-blocks of terms.
+- Programs are **typable**, but without primitive types or predefined type
+systems;
+- Both computation and typing rely on the same mechanism: **term unification**.
+- It is multi-paradigm:
 
-It is multi-paradigm:
-- _logic programs_ called "constellations" are the elementary blocks of
-programming;
-- _functional programs_ correspond to layered constellations enforcing an order
-of interaction;
-- _imperative programs_ are iterative recipes constructing constellations;
-- _objects_ are ways to structure constellations.
+| Paradigm        | Stellogen equivalent                                     |
+| --------------- | ---------------------------------------------------------|
+| Logic           | Constellations (elementary blocks)                       |
+| Functional      | Layered constellations enforcing order of interaction    |
+| Imperative      | Iterative recipes for building constellations            |
+| Object-oriented | Structured constellations                                |
 
 ## Influences
 
-It draws (or try to draw) inspiration from:
-- Prolog/Datalog (for unification-based computation and constraint solving);
-- Smalltalk (for message-passing, object-oriented paradigm and minimalism);
-- Coq (for proof-as-program paradigm and iterative programming with tactics);
-- Scheme/Racket (for minimalism and metaprogramming);
-- Shen (for its optional type systems and its "power and responsibility"
-philosophy).
+Stellogen borrows ideas from several traditions: from **Prolog/Datalog** for
+the power of unification; from **Smalltalk** for the minimalism of
+message-passing and objects; from **Rocq** for the proof-as-program paradigm;
+from **Scheme/Racket** for the spirit of metaprogramming; and from **Shen** for
+the philosophy of optional type systems where *power comes with responsibility*.
+
+## How it works
 
-## Syntax samples
+The language uses extended S-expressions.
 
-Finite state machine
+Here is a commented example of the definition of a finite state machine
+accepting words ending with `00`.
 
 ```
+' We define a macro 'spec' for type definition
+' It is just an alias for the definition [:=]
 (new-declaration (spec X Y) (:= X Y))
+
+' We define a macro for type assertion
 (new-declaration (:: Tested Test)
-  (== @(interact @#Tested #Test) ok))
+  (== @(interact @#Tested #Test) ok)) ' triggers interaction and expects [ok]
 
+' The type [binary] is defined as a set of three interactive tests
+' According to the previous macro, the tests pass when interaction gives [ok]
 (spec binary {
-  [(-i []) ok]
-  [(-i [0|X]) (+i X)]
-  [(-i [1|X]) (+i X)]})
-
-'input words
-(:= e (+i []))        (:: e binary)
-(:= 0 (+i [0]))       (:: 0 binary)
-(:= 000 (+i [0 0 0])) (:: 000 binary)
-(:= 010 (+i [0 1 0])) (:: 010 binary)
-(:= 110 (+i [1 1 0])) (:: 110 binary)
-
-'''
-automaton accepting words ending with 00
-'''
-(:= (initial Q) [(-i W) (+a W Q)])
-(:= (accept Q) [(-a [] Q) accept])
-(:= (if read C1 on Q1 then Q2) [(-a [C1|W] Q1) (+a W Q2)])
-
-(:= a1 {
-  #(initial q0)
-  #(accept q2)
-  #(if read 0 on q0 then q0)
-  #(if read 0 on q0 then q1)
-  #(if read 1 on q0 then q0)
-  #(if read 0 on q1 then q2)})
-
-(:= kill (-a _ _))
-
-(show (process (interact @#e #a1)   #kill))
-(show (process (interact @#000 #a1) #kill))
-(show (process (interact @#010 #a1) #kill))
-(show (process (interact @#110 #a1) #kill))
+  [(-i []) ok]          ' returns [ok] on empty list
+  [(-i [0|X]) (+i X)]   ' matches on [0] and checks the tail
+  [(-i [1|X]) (+i X)]}) ' matches on [1] and checks the tail
+                        ' otherwise the term remains unchanged
+
+' We define some words
+(:= word1 (+i [0 1 1]))
+(:= word2 (+i [2 3]))
+
+' succeeds -> [ok] is obtained on interaction with test [binary]
+(:: word1 binary)
+
+' fails
+' (:: word2 binary)
 ```
 
 More examples can be found in `examples/`.
@@ -83,8 +100,10 @@ This project is still in development, hence the syntax and features
 are still changing frequently.
 
 To learn more about the current implementation of stellogen:
-- French guide (official): https://tsguide.refl.fr/
-- English guide: https://tsguide.refl.fr/en/
+
+https://github.com/engboris/stellogen/wiki/Basics-of-Stellogen
+
+A more complete guide is in production.
 
 # Use
 

diff --git a/guide/en/.gitignore b/guide/en/.gitignore
diff --git a/guide/en/Makefile b/guide/en/Makefile
diff --git a/guide/en/book.toml b/guide/en/book.toml
diff --git a/guide/en/src/SUMMARY.md b/guide/en/src/SUMMARY.md
diff --git a/guide/en/src/imperative/processes.md b/guide/en/src/imperative/processes.md
diff --git a/guide/en/src/introduction/introduction.md b/guide/en/src/introduction/introduction.md