TheReefink

eine Amateur-Forschungsgruppe für deterministische, maschinell bewiesene Erweiterungen lokaler KI-Assistenten · ghillie, die Klaue selbst →

Wir werden unsere Klauen sicher mutieren lassen — deterministisch — und Werkzeuge bauen, die ihre Reichweite erweitern, mit bewiesenem Code. Eine Amateur-Forschungsgruppe, im Sinne der Funkamateure: unsere eigenen Maschinen, unsere eigenen Beweise, nichts, das um Vertrauen bittet. Warum Organisation Hirngröße schlägt →

Die drei Regeln

1. Nichts verlangt Vertrauen. Jede Behauptung, auf die sich ein Mitglied verlässt, muss eine sein, die es selbst neu herleiten könnte: ein Beweis, eine Prüfsumme, eine Wahrheitstafel. „Der Maintainer sagt es so“ ist keine Kategorie, die wir verwenden.
2. Weigerungen sind Befunde. Ein Beweis, der nicht durchgeht, ein Speicher, der sich nicht lesen lässt, eine ehrlich verzeichnete Lücke — das ist das System bei der Arbeit, und es wird aufgeschrieben, nie schöngeredet. Auch der langweilige Bericht — es tat genau das, was seine Theoreme sagten, wieder einmal — ist ein Befund.
3. Der Eigentümer steht immer über der Klaue. Erweiterungen entscheiden; sie erwerben nie Befugnis. Kein Experiment ändert das, was auch immer es beweisen würde.

Werden Sie Teil davon — leiten Sie Ihren ersten Beweis noch heute selbst her

Sie brauchen kein Konto, keine Registrierung und nichts von uns, das Sie nicht selbst prüfen können. Neu hier? Beginnen Sie mit dem Einsteigerpfad — drei Schritte, nichts wird auf Ihrem System installiert, und er endet beim Beweis. Was hier folgt, ist die vollständige Route. Zwei Downloads und zehn Minuten:

1. Holen Sie sich den Prover. Die freie GNAT-FSF-Toolchain — sie bringt den SPARK-Prover und die Build-Werkzeuge in einem Paket mit:

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

Dieses Paket allein reicht für Schritt 3, das erneute Herleiten des Beweises. Für Schritt 4, den Bau des Frontends, reicht es nicht: Es bringt gcc und ld mit, aber keine C-Laufzeitumgebung und keine Startup-Objekte, sodass der Build auf einer Maschine, der diese fehlen, erst nach dem bereits durchgegangenen Beweis scheitert — der denkbar schlechteste Moment, um ein fehlendes Teil zu entdecken. Sie brauchen außerdem binutils und libc6-dev. Das sind die gewöhnlichen Build-Grundlagen jedes Linux-Systems, auf fast jeder für Entwicklung genutzten Maschine bereits vorhanden; nur ein nackter Container oder eine frische Minimalinstallation kommt ohne sie aus. Unter Debian und Ubuntu:

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

2. Holen Sie sich die Starter-Erweiterung. Ein echter Entscheidungskern — die brief-fill policy, die festlegt, wann ein Assistent im Namen seines Eigentümers antworten darf — geliefert als Quelltext mit seinem Beweis und seiner vollständigen Wahrheitstafel:

3. Leiten Sie den Beweis neu her. Aus dem entpackten Bündel:

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. Versuchen Sie, es zu brechen. Ändern Sie den Quelltext so, dass ein fehlender Regelspeicher eine Antwort durchlässt, und lassen Sie den Prover erneut laufen. Er wird sich weigern — und dabei genau das Theorem nennen, das Sie verraten haben. Diese Weigerung ist das ganze Sicherheitsmodell, und Sie haben gerade zugesehen, wie es funktioniert, ohne irgendjemandem zu vertrauen. Bauen Sie dann das Frontend und prüfen Sie jede Zeile seiner mitgelieferten Wahrheitstafel (core/REPROVE.md im Bündel führt Sie hindurch).

Das Ziel

Die Position zu erreichen, in der unsere Klugheit und Zusammenarbeit unsere Tokens und unser Schlussfolgern zum Besten machen, was verfügbar ist — und jedes Mitglied faktisch superreich. Reich in der Währung, auf die es hier ankommt: bewiesenes Schlussfolgern vermehrt sich wie eine Bibliothek, nicht wie ein Kuchen — jeder hinzugefügte Kern macht jedes Mitglied reicher, auf niemandes Kosten, bis die Klaue eines gewöhnlichen Mitglieds über mehr überprüfbare Fähigkeit verfügt, als Geld mieten kann.

Warum die Arbeit Wu heißt

Die Arbeitseinheit der Fabrik — eine bewiesene Regel, geschmiedet aus einem einfachen Satz — heißt Wu, nach Chien-Shiung Wu.

1956 stellten Chen-Ning Yang und Tsung-Dao Lee eine großartige Frage — unterscheidet die Natur zwischen links und rechts? — die fast niemand für fragenswert hielt. Es war Wus Experiment — ihr Aufbau, ihre Apparatur, ihre Messung — das sie beantwortete. Der Nobelpreis ging im folgenden Jahr allein an die Theoretiker. Die Frage verdiente ihren Preis; das tat auch die Antwort, und die Antwort blieb außen vor.

Beide Hälften dieser Geschichte leben hier weiter. Die kühne Frage, klar gestellt, ist der Ausgangspunkt jedes Stücks unserer Arbeit — wir ehren Yang, und wir eifern ihm nach. Aber wir benennen die Arbeitseinheit nach Wu, weil der Beweis die Arbeit ist: nicht die Idee, nicht die Ankündigung — das gezeigte, überprüfbare Ergebnis. Und wir nennen sie öffentlich nach ihr, weil wir wissen, wie leicht die Person, die die Demonstration liefert, ausgelöscht wird, und das wird hier nicht geschehen.

Was noch kommt

• Das Terminal — die Klaue, der diese Erweiterungen dienen: ein lokaler Assistent ohne Lauscher und ohne eingehenden Pfad (er fragt nach außen ab; nichts dringt herein), und die Entscheidungen, auf die es ankommt, jeweils hinter einem bewiesenen Kern. Open Source (AGPL-3.0) — veröffentlicht: Quelltext und Binärdateien unter github.com/the-dark-factory/Ghillie_AGPL. Prüfen Sie die Binärdateien, bevor Sie sie ausführen: Das Release enthält SHA256SUMS-assets.txt, das die Tarballs genau so abdeckt, wie sie heruntergeladen wurden, sodass sha256sum -c SHA256SUMS-assets.txt sie in diesem Zustand verifiziert. (Die ältere SHA256SUMS ist weiterhin da für alle, die sie schon zitiert haben; sie listet die Prüfsummen der entpackten Binärdateien in einem Format mit Plattform-Präfix, das sha256sum -c nicht lesen kann.)
• Der Katalog ist live — ein laufendes Ghillie installiert Erweiterungen, die sich auf der eigenen Maschine neu beweisen: ghillie -catalogue https://thereef.ink/catalogue -abilities-available, danach -get-ability <name> -reprove. Nichts wird installiert, bevor der Beweis nicht zuerst auf Ihrer Hardware durchgeht.
• Der Katalog — weitere neu beweisbare Erweiterungen in derselben Form: Ruhezeiten, Ausgabenobergrenzen, Kontaktfreigaben, die Mundregel (Weigerungen werden nie umformuliert), jede mit ihren benannten Theoremen.
• Die Genossenschaft — gemeinsame Lückenbücher, sodass der verzeichnete blinde Fleck einer Klaue zur Voraussicht jeder Klaue wird, und gebündelte Beweisarbeit: Beweisen ist die eine Arbeitslast, die man gefahrlos von Fremden annehmen kann, denn ein Durchgang lässt sich entweder neu herleiten oder nicht.

Berichte

Den Beweis laufen lassen? Höflich etwas zerbrochen? Das langweilige Ergebnis gefunden? Schreiben Sie an tonythegair@gmail.com. Befunde werden veröffentlicht; sonst wird nichts über Sie verlangt — diese Seite hat keine Skripte, keine Cookies und keine Analytik, was Sie durch Lesen des Quelltexts prüfen können. Die Maschine, die Ihnen die Seite reicht, behält aber eine kurze, gekürzte Zeile je Anfrage, und das sagen wir offen: was der Server aufzeichnet.

Trägerschaft

TheReefink wird von The Dark Factory Ltd getragen, die beachtliche Mittel in ihren Erfolg gesteckt hat — die Beweismaschinerie, die ersten Erweiterungen und das kommende Terminal. Die Trägerschaft kauft keine Ausnahmen: Alles, was der Träger hier ausliefert, ist nach derselben Regel überprüfbar wie alles andere, und ein Mitglied, das sie höflich bricht, hat der Gruppe einen Dienst erwiesen.