Jusqu’ici, dans cet arc, on a suivi une seule moitié du travail : apprendre au compilateur à lire. Un programme, c’est un arbre montrait comment le texte devient un AST ; le tokenizer comment les octets deviennent des mots. Lire, découper, comprendre.

Mais comprendre un programme, ce n’est que la première moitié d’un compilateur. L’autre moitié, c’est écrire — produire, à la sortie, du code que le processeur exécute vraiment. Un traducteur qui sait comprendre l’anglais n’a fait que la moitié du chemin ; le jour où il sait rédiger en anglais, lettre par lettre, dans le bon alphabet, là il traduit pour de vrai.

Ce billet raconte ce jour-là, côté verbose. Une règle verbose — pas le compilateur Rust en dessous, une règle écrite dans le langage — sait maintenant écrire du x86-64, octet par octet, jusqu’à produire un exécutable Linux complet. On tape ./a.out, il imprime 120.

⚠️ Honnêteté d’abord : ça vit sur une branche de travail (feat/self-hosting), pas encore mergé ni taggé. C’est vérifié (suite de tests verte, exécution réelle en mémoire, bench mesuré), mais ce n’est pas dans une version publiée. Et ça couvre un sous-langage — l’arithmétique scalaire, pas tout verbose. J’y reviens à la fin.

Les deux moitiés

   LIRE  (front-end, les chapitres précédents)
   texte ──tokenizer──► mots ──parser──► arbre (AST)
                                            │
   ÉCRIRE (back-end, ce billet)             ▼
   arbre ──générateur──► octets x86-64 ──ELF──► ./a.out

La nouveauté est la flèche du bas. Et le point qui compte : ce générateur est lui-même une règle verbose. Le compilateur Rust (verbosec) ne fait que l’exécuter. Le code machine, ce sont les règles verbose qui le pondent.

On part d’un exemple, et on le suit jusqu’au bout

Le programme le plus parlant, c’est la factorielle — parce qu’elle se rappelle elle-même :

@intention "calculer n!"
@proof termination decreasing : n
rule fact (n : number [0, 20]) -> number {
  if n == 0 then 1 else n * fact(n - 1)
}

Deux choses à noter avant de descendre. Le @proof termination decreasing : n : verbose exige une preuve que la récursion s’arrête (ici : n décroît à chaque appel). Et le [0, 20] : le domaine de n est borné, déclaré. Ce sont les garde-fous habituels du langage — on les garde même quand on descend jusqu’aux octets.

Maintenant la descente. Le générateur traverse l’arbre et, pour chaque nœud, crache la séquence x86-64 correspondante. En lisant les valeurs concrètes :

  nœud de l'arbre              ce que la règle émet (idée)
  ─────────────────            ───────────────────────────
  n == 0                       cmp ; sete        → vrai/faux dans un registre
  if … then … else …          jz over_then ; <then> ; jmp end ; over_then: <else> ; end:
  n * fact(n - 1)              <calcule fact(n-1)> ; imul          → multiplie
  fact(n - 1)                  call <offset>      → s'appelle elle-même

Le jz/jmp du if portent un offset calculé : on ne connaît la distance du saut qu’une fois les deux branches émises, donc le générateur passe deux fois (mesurer, puis écrire) — exactement comme on numérote les pages d’un livre seulement après l’avoir mis en page.

La récursion, vue comme une pile d’assiettes

Le vrai jalon, c’est le call/ret. Quand fact s’appelle elle-même, chaque appel empile son contexte et le récupère au retour. fact(3) ressemble à une pile d’assiettes qu’on monte, puis qu’on redescend en multipliant :

  on monte                    on redescend (ret)
  fact(3)  n=3                 3 × 2 = 6   ◄── résultat final
   └ fact(2)  n=2              2 × 1 = 2
      └ fact(1)  n=1           1 × 1 = 1
         └ fact(0)  n=0  ─► 1  (cas de base, on arrête de monter)

Avant cette brique, la règle savait émettre + − × neg sans branchement. Maintenant elle émet de vrais call <offset_relatif> et ret : le code se référence lui-même. C’est la première fois qu’une règle écrite en verbose produit du code machine qui s’appelle lui-même — et qui calcule fact(5) = 120 quand on l’exécute.

De la blob d’octets à un vrai exécutable

Émettre les bons octets, c’est bien. Mais des octets dans un buffer ne s’exécutent pas tout seuls — il faut les emballer pour que Linux accepte de les lancer. Cet emballage, c’est le format ELF, et la règle le génère maintenant en entier.

Un ELF, c’est comme un colis prêt à expédier :

  ┌─────────────────────────────────────────┐
  │ en-tête ELF64        ← « ceci est un     │
  │                         exécutable Linux »│
  ├─────────────────────────────────────────┤
  │ program header LOAD  ← « charge ça en    │
  │                         mémoire, en r+x » │
  ├─────────────────────────────────────────┤
  │ _start               ← le point d'entrée :│
  │   call main             appelle main,     │
  │   rax → itoa            convertit le       │
  │   sys_write             résultat en texte, │
  │   sys_exit              l'imprime, sort     │
  ├─────────────────────────────────────────┤
  │ code de main, de fact ← le calcul lui-même│
  └─────────────────────────────────────────┘

Pas de section, pas de symbole, pas de bibliothèque liée. Quelques centaines d’octets, et c’est tout. La dernière brique (b8) a ajouté itoa — la conversion i64 → décimal ASCII — en code machine : sans elle, l’exécutable calculait 120 mais ne savait pas l’afficher. Désormais :

$ ./verbosec examples/factorial.verbose --run lower factorial 5 > a.out
$ chmod +x a.out
$ ./a.out
120

Plus aucune dépendance à verbosec pour exécuter le résultat. Le binaire est autonome.

Le bench honnête : où ça gagne, où ça perd

La question qui traîne depuis le début — « un binaire produit comme ça, ça vaut quoi face à C, Rust, Go ? » — a maintenant une réponse mesurée (Ubuntu 24.04, gcc 13.3, rustc 1.90, go 1.25.4) :

  trivial (imprime une constante, sort)
              taille      wall(ms)  RSS(kB)  syscalls
  verbose        512       0.19      352        2
  gcc        706 584       0.24      664       17
  rustc    3 871 984       0.57    2 112       62
  go       2 254 335       1.28    2 132      228

  fib(40) = 102334155  (récursion profonde — débit de calcul)
              taille      wall(ms)  RSS(kB)  syscalls
  verbose        635      ~713       352        2
  gcc        706 584      ~135       664       17
  rustc    3 872 832      ~224     2 216       62
  go       2 254 624      ~380     2 232      406

Lisons-le honnêtement, dans les deux sens.

Ce qui gagne — par construction. Le binaire verbose est ~1100 à 1380× plus petit que le gcc -static, ~6000× plus petit que rustc, ~3500× plus petit que go. Deux syscalls (write + exit) contre 17 à 228. RSS divisée par 2 à 6. Pourquoi ? Parce qu’il n’y a pas de runtime : rien à initialiser, pas d’allocateur global, pas de bibliothèque dynamique. Ce sont précisément les axes sur lesquels le langage a bâti sa thèse — et ils sont audit-defensible : il n’y a presque rien à auditer.

Ce qui perd — assumé. Sur fib(40), verbose met ~5× le temps de gcc. La blob produite n’a vu aucun optimiseur : pas d’allocation de registres, pas d’inlining, pas de constant folding au-delà de l’AST. C’était une décision de conception, pas un oubli : un émetteur direct, auditable ligne à ligne, pas un backend LLVM. Le coût de calcul est le prix de cette lisibilité — et on le publie au lieu de le cacher.

Ce qui n’est pas encore là

  • C’est un sous-langage : l’arithmétique scalaire (+ − × ÷ %, comparaisons, and/or, if/else, let, appels récursifs). Pas de chaînes, pas d’I/O, pas de services, pas de TLS. La calculatrice, pas tout verbose.
  • C’est sur une branche, non mergé, non taggé.
  • Pas d’optimisation — délibérément reportée pour garder chaque octet auditable.

Pourquoi je le raconte quand même

Parce que la forme du résultat compte plus que sa complétude. Une règle écrite dans le langage produit un exécutable Linux autonome, qui calcule par récursion réelle et imprime sa réponse — et un bench honnête le situe sans bluff. Ce n’est pas « verbose bat gcc » ; c’est « voici exactement ce que verbose achète, et ce qu’il coûte, mesuré ». La moitié lire et la moitié écrire se rejoignent d’un cran. Le reste du sous-langage — text, bytes, match, les bornes runtime — est la suite naturelle.