TheReefink

un groupe de recherche amateur pour des extensions déterministes et prouvées par machine, destinées aux assistants IA locaux · ghillie, la griffe elle-même →

Nous allons faire muter nos griffes en sûreté — de façon déterministe — et construire des outils qui étendent leur portée, avec du code prouvé. Un groupe de recherche amateur, au sens des radioamateurs : nos propres machines, nos propres preuves, rien qui demande qu'on lui fasse confiance. Pourquoi l'organisation l'emporte sur la taille du cerveau →

Les trois règles

1. Rien ne demande qu'on lui fasse confiance. Toute affirmation sur laquelle un membre s'appuie doit être une affirmation qu'il pourrait re-dériver lui-même : une preuve, une empreinte, une table de vérité. « Le mainteneur le dit » n'est pas une catégorie que nous utilisons.
2. Les refus sont des constats. Une preuve qui ne se décharge pas, un dépôt qu'on ne peut pas lire, un manque honnêtement consigné — ce sont là le système qui fonctionne, et ils sont notés, jamais lissés. Le rapport ennuyeux — cela a fait exactement ce que ses théorèmes disaient, encore une fois — est aussi un constat.
3. Le propriétaire prime toujours sur la griffe. Les extensions décident ; elles n'acquièrent jamais d'autorité. Aucune expérience ne change cela, quoi qu'elle puisse prouver.

Rejoignez-nous — re-dérivez votre première preuve aujourd'hui

Vous n'avez besoin d'aucun compte, d'aucune inscription, et de rien venant de nous que vous ne puissiez vérifier. Nouveau ici ? Commencez par le parcours débutant — trois étapes, rien d'installé sur votre système, et cela s'arrête à la preuve. Ce qui suit ici est le parcours complet. Deux téléchargements et dix minutes :

1. Procurez-vous le prouveur. La chaîne d'outils gratuite GNAT FSF — elle porte le prouveur SPARK et les outils de construction en un seul paquet :

https://github.com/alire-project/GNAT-FSF-builds/releases
  (gnatprove-x86_64-linux, -darwin, or -windows64 — unpack anywhere)

Ce seul paquet suffit pour l'étape 3, re-dériver la preuve. Il ne suffit pas pour l'étape 4, construire le front : il fournit gcc et ld mais aucun runtime C ni objets de démarrage, si bien que sur une machine qui en est dépourvue, la construction échoue après que la preuve s'est déjà déchargée — le pire moment possible pour découvrir qu'une pièce manque. Il vous faut aussi binutils et libc6-dev. Ce sont les éléments de base ordinaires de tout système Linux, déjà présents sur presque toute machine utilisée pour le développement ; ce sont un conteneur nu ou une installation minimale fraîche qui en sont dépourvus. Sur Debian et Ubuntu :

sudo apt-get install binutils libc6-dev
# Fedora/RHEL: the equivalents are binutils and glibc-devel

2. Procurez-vous l'extension de démarrage. Un vrai noyau de décision — la brief-fill policy, qui décide quand un assistant peut répondre au nom de son propriétaire — livré en source avec sa preuve et sa table de vérité complète :

3. Re-dérivez la preuve. Depuis l'archive décompressée :

cd brief-fill-policy/core/src
gnatprove -P proof.gpr -f -U --level=2
# success: "0 unproved" — four named theorems, discharged on YOUR machine:
#   NEVER-FILLED-WITHOUT-A-LICENSING-RULE
#   AN-ABSENT-STORE-NEVER-LETS-A-FILL-THROUGH
#   NOTHING-INVENTED-EVER
#   NOTHING-ASKED-THAT-A-RULE-ALREADY-ANSWERS

4. Essayez de la casser. Modifiez la source pour qu'un dépôt de règles absent laisse passer une réponse, puis relancez le prouveur. Il refusera — en nommant le théorème exact que vous avez trahi. Ce refus est tout le modèle de sécurité, et vous venez de le voir fonctionner sans faire confiance à personne. Construisez ensuite le front et vérifiez chaque ligne de sa table de vérité fournie (core/REPROVE.md dans l'archive vous guide).

Le but

Atteindre la position où notre intelligence et notre coopération font de nos jetons et de notre raisonnement ce qu'il y a de meilleur disponible — et de chaque membre, en pratique, quelqu'un de très riche. Riche dans la monnaie qui compte ici : le raisonnement prouvé s'accumule comme une bibliothèque, pas comme un gâteau à partager — chaque noyau ajouté enrichit chaque membre sans appauvrir personne, jusqu'à ce que la griffe d'un membre ordinaire commande plus de capacité vérifiable que l'argent ne peut en louer.

Pourquoi le travail se nomme Wu

L'unité de travail de l'usine — une règle prouvée, forgée à partir d'une simple phrase — s'appelle un Wu, d'après Chien-Shiung Wu.

En 1956, Chen-Ning Yang et Tsung-Dao Lee ont posé une question magnifique — la nature distingue-t-elle la gauche de la droite ? — que presque tout le monde jugeait indigne d'être posée. C'est l'expérience de Wu — sa conception, son montage, sa mesure — qui y a répondu. Le prix Nobel, l'année suivante, est allé aux seuls théoriciens. La question méritait son prix ; la réponse aussi le méritait, et la réponse a été laissée de côté.

Les deux moitiés de cette histoire vivent ici. La question audacieuse, posée simplement, est le point de départ de chaque pièce de notre travail — nous honorons Yang, et nous l'imitons. Mais nous nommons l'unité de travail d'après Wu, parce que la preuve est le travail : pas l'idée, pas l'annonce — le résultat démontré, vérifiable. Et nous la nommons d'après elle publiquement parce que nous savons avec quelle facilité la personne qui fait la démonstration se fait effacer, et cela n'arrivera pas ici.

Ce qui s'en vient

• Le terminal — la griffe que ces extensions servent : un assistant local sans aucun écouteur et sans chemin entrant (il interroge vers l'extérieur ; rien n'entre), et les décisions qui comptent chacune derrière un noyau prouvé. Open source (AGPL-3.0) — publié : source et binaires sur github.com/the-dark-factory/Ghillie_AGPL. Vérifiez les binaires avant de les exécuter : la version porte SHA256SUMS-assets.txt, qui couvre les archives telles que téléchargées, si bien que sha256sum -c SHA256SUMS-assets.txt les vérifie telles quelles. (L'ancien SHA256SUMS est toujours là pour quiconque l'aurait cité ; il liste les empreintes des binaires décompressés dans un format préfixé par plateforme que sha256sum -c ne peut pas lire.)
• Le catalogue est en ligne — un ghillie en fonctionnement installe des extensions qui se re-prouvent sur sa propre machine : ghillie -catalogue https://thereef.ink/catalogue -abilities-available, puis -get-ability <name> -reprove. Rien ne s'installe tant que sa preuve ne s'est pas déchargée sur votre matériel au préalable.
• Le catalogue — d'autres extensions re-prouvables dans le même moule : heures calmes, plafonds de dépense, autorisations de contact, la règle de la bouche (les refus ne sont jamais reformulés), chacune avec ses théorèmes nommés.
• La coopérative — des registres de manques partagés, si bien que l'angle mort consigné par une griffe devient la prévoyance de toutes les autres, et un travail de preuve mis en commun : prouver est la seule charge de travail que l'on puisse accepter sans risque d'inconnus, parce qu'une décharge re-dérive, ou elle ne re-dérive pas.

Rapports

Vous avez lancé la preuve ? Cassé quelque chose poliment ? Trouvé le résultat ennuyeux ? Écrivez à tonythegair@gmail.com. Les constats sont publiés ; rien d'autre sur vous n'est demandé — cette page n'a ni scripts, ni cookies, ni mesure d'audience, ce que vous pouvez vérifier en la lisant. La machine qui vous sert la page garde bien une courte ligne tronquée par requête, et le dit sans détour : ce que le serveur enregistre.

Patronage

TheReefink est patronné par The Dark Factory Ltd, qui a consacré des ressources considérables à sa réussite — la machinerie de preuve, les premières extensions, et le terminal à venir. Le patronage n'achète aucune exception : tout ce que le patron livre ici est vérifiable selon la même règle que tout le reste, et un membre qui le casse poliment a rendu service au groupe.