Tagged 2026-05-26. 12 commits depuis v0.5.0. La release qui ferme Phase B, ouvre Phase C (le compilateur commence à prouver la terminaison), et ajoute l’état mutable aux services.

Shipped

Phase C — le compilateur prouve la terminaison (3 slices)

  • What — trois slices de preuve structurelle. Le compilateur verbose vérifie maintenant que les règles récursives terminent, au lieu de simplement le breadcrumber. Slice 1 : preuve de terminaison structurelle pour les types concept_group (listes chaînées, arbres). Slice 2 : preuve que un champ numérique décroît à chaque appel récursif (n.v - 1 dans factorial). Slice 3 : preuve qu’un champ numérique croît vers une borne max.
  • Why — dans l’article #1 de la série éducative, on avait documenté le breadcrumb : “la profondeur est bornée par la plage déclarée, mais ce n’est pas une preuve mathématique de terminaison.” Phase C remplace ce breadcrumb par une vérification réelle.
  • Choice — vérification au compile-time, pas au runtime. Pas de code machine supplémentaire émis. Si la preuve échoue, la compilation est refusée. Si elle réussit, le breadcrumb disparaît.

Mutable service state (PR #47)

  • What — blocs state: (champs numériques initialisés au démarrage) et after: (mutations appliquées après chaque requête HTTP). counter_service.verbose : 937 octets, chaque requête retourne count:N et incrémente.
  • Why — un service HTTP sans état n’a qu’un intérêt limité. Le compteur est le cas minimal qui démontre la persistance inter-requêtes.
  • Choice — état stocké dans des slots [rbp - N] du frame du service. Mode concurrency: forked hérite l’état initial via COW mais les mutations ne remontent pas au parent.

Phase B fermée — text payloads dans les variants (PR #48)

  • What — les variantes de concept_group peuvent maintenant porter des payloads texte. Le label_tree worked example (#50) construit un arbre dont les nœuds portent des labels texte.
  • Why — un arbre de syntaxe (AST) a des nœuds avec des noms (texte). Sans payload texte, les types récursifs ne pouvaient représenter que des structures numériques.
  • Choice — les textes dans l’arène utilisent le même format (ptr, len) que les retours texte de Phase A.5.2.

Recursive text scanner (PR #53)

  • What — scan_word.verbose : premier scanner texte récursif natif. Parcourt une chaîne byte par byte, s’arrête au premier espace.
  • Why — le tokenizer auto-hébergé aura besoin exactement de ce pattern.
  • Choice — même ABI call/ret que factorial. Le champ pos : number [0, 256] borne la profondeur. Preuve de terminaison via increasing : pos.

Text input fields + let bindings (PRs #52, #54)

  • What — les règles récursives acceptent des champs texte en entrée et supportent les let bindings. Les callables récursifs sont fonctionnellement complets pour le scanning.
  • Why — scan_word en avait besoin.
  • Choice — text inputs via pointer-in-rdi. Let bindings allouent des slots supplémentaires dans le frame.

What we learned

Phase C transforme un commentaire en une vérification. Le decreasing: v existait dans le source depuis v0.4.0. Pendant 3 releases, c’était une annotation documentaire. Phase C change ça : le vérificateur suit l’expression récursive, confirme que le champ cité décroît (ou croît vers une borne), et refuse de compiler si la preuve ne tient pas. Le source n’a pas changé. Le binaire n’a pas changé. Ce qui a changé, c’est la confiance que le compilateur a dans le programme.

Le scanner récursif montre que verbose approche l’auto-hébergement. scan_word est le premier programme verbose qui fait du text-processing récursif — le même pattern qu’un tokenizer.

Open

  • Phase C : preuves multi-field et types non-numériques
  • Phase D (self-hosting campaign) : estimé 6-12 mois après que Phase C ferme
  • Champs state: de type texte différés

How to try

git clone https://github.com/verbose-org/verbose
cd verbose
cargo run -- examples/factorial.verbose --native /tmp/fact --run fact --stream
echo '{"v":5}' | /tmp/fact

Ou télécharger le binaire précompilé depuis la page release v0.6.0.