TheReefink

אַ ליבהאָבערישע פֿאָרש-גרופּע פֿאַר דעטערמיניסטישע, מאַשין-באַוויזענע פֿאַרברייטערונגען צו אָרטיקע קינסטלעכע-אינטעליגענץ-אַסיסטענטן · ghillie, די לאַפּע אַליין →

מיר גייען זיכער מוטירן אונדזערע לאַפּעס — דעטערמיניסטיש — און בויען געצייג וואָס פֿאַרברייטערט זייער רײַכווייט, מיט באַוויזענעם קאָד. אַ ליבהאָבערישע פֿאָרש-גרופּע, אין זין פֿון אַ ראַדיאָ-ליבהאָבער: אונדזערע אייגענע מאַשינען, אונדזערע אייגענע באַווײַזן, גאָרנישט וואָס בעט צו ווערן געטרויט. Why organisation beats brain size →

די דרײַ כּללים

1. גאָרנישט בעט צוטרוי. יעדע טענה וואָס אַ מיטגליד פֿאַרלאָזט זיך אויף מוז זײַן איינע וואָס ער קען אַליין אַרויסלייטן: אַ באַווײַז, אַ קאָנטראָל-סומע, אַ וואָר-טאַבעלע. „דער פֿאַרוואַלטער זאָגט אַזוי" איז ניט קיין קאַטעגאָריע וואָס מיר ניצן.
2. אָפּווייזונגען זענען געפֿינסן. אַ באַווײַז וואָס קען זיך ניט אַרויסלייטן, אַן אָפּלאַגער וואָס מען קען ניט לייענען, אַ ליקנע ערלעך פֿאַרשריבן — דאָס זענען די סיסטעם בײַ דער אַרבעט, און זיי ווערן פֿאַרשריבן, קיינמאָל ניט אויסגעגלעט. דער נודנער באַריכט — עס האָט געטאָן פּונקט וואָס זײַנע טעאָרעמען האָבן געזאָגט, ווידער אַ מאָל — איז אויך אַ געפֿינס.
3. דער באַזיצער איז תּמיד העכער פֿון דער לאַפּע. פֿאַרברייטערונגען באַשליסן; זיי קריגן קיינמאָל קיין סמכות. קיין עקספּערימענט טוישט דאָס ניט, וואָס עס זאָל ניט באַווײַזן.

ווער אַ טייל דערפֿון — לייט אַרויס דײַן ערשטן באַווײַז הײַנט

דו דאַרפֿסט קיין קאָנטע ניט, קיין רעגיסטראַציע ניט, און גאָרנישט פֿון אונדז וואָס דו קענסט ניט נאָכקוקן. נײַ אין דעם? אָנהייב מיטן וועג פֿאַרן אָנהייבער — דרײַ טריט, גאָרנישט אינסטאַלירט אויף דײַן סיסטעם, און עס שטעלט זיך אָפּ בײַם באַווײַז. וואָס פֿאָלגט דאָ איז דער גאַנצער וועג. צוויי אַראָפּלאָדן און צען מינוט:

1. נעם דעם פּרוּווער. דער פֿרײַער GNAT FSF-געצייגקייט — זי טראָגט דעם SPARK-פּרוּווער און די בוי-געצייגן אין איין פּעקל:

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

דאָס פּעקל אַליין איז גענוג פֿאַר טריט 3, אַרויסלייטן דעם באַווײַז. עס איז ניט גענוג פֿאַר טריט 4, בויען דעם פֿראָנט: עס טראָגט gcc און ld, אָבער קיין C-לויפֿצײַט און קיין אָנהייב-אָביעקטן ניט, אַזוי אויף אַ מאַשין וואָס פֿעלט זיי, פֿאַלט דער בוי דורך נאָכדעם דער באַווײַז האָט זיך שוין אַרויסגעלייט — דער ערגסטער מעגלעכער רגע צו געפֿינען אַ פֿעלנדיקן טייל. דו דאַרפֿסט אויך binutils און libc6-dev. דאָס זענען די געוויינטלעכע בוי-יסודות פֿון יעדער לינוקס-סיסטעם, שוין פֿאַראַן אויף כּמעט יעדער מאַשין וואָס ווערט גענוצט פֿאַר אַנטוויקלונג; עס איז אַ נאַקעטער קאָנטיינער אָדער אַ פֿרישע מינימאַלע אינסטאַלאַציע וואָס פֿעלט זיי. אויף Debian און Ubuntu:

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

2. נעם די אָנהייב-פֿאַרברייטערונג. אַ ריכטיקער באַשלוס-קערן — די brief-fill policy, וואָס באַשליסט ווען אַן אַסיסטענט מעג ענטפֿערן אין נאָמען פֿון זײַן באַזיצער — צוגעשטעלט ווי מקור-קאָד מיט זײַן באַווײַז און זײַן פֿולער וואָר-טאַבעלע:

3. לייט אַרויס דעם באַווײַז. פֿון דעם אַנטפּאַקטן בינטל:

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. פּרוּוו עס צעברעכן. רעדאַקטיר דעם מקור-קאָד אַזוי אַז אַ פֿעלנדיקער כּלל-אָפּלאַגער לאָזט אַן ענטפֿער דורך, און לויף דעם פּרוּווער נאָך אַ מאָל. ער וועט זיך אָפּווײַזן — נעמענדיק דעם פּינקטלעכן טעאָרעם וואָס דו האָסט פֿאַרראַטן. יענע אָפּווייזונג איז דער גאַנצער זיכערהייט-מאָדעל, און דו האָסט נאָר וואָס באַטראַכט אים אַרבעטן אָן צו טרויען קיינעם. דערנאָך בוי דעם פֿראָנט און קאָנטראָליר יעדע שורה פֿון זײַן צוגעשיקטער וואָר-טאַבעלע (core/REPROVE.md אין דעם בינטל פֿירט דיך דורך עס).

דער ציל

צו דערגרייכן דעם פּונקט וווּ אונדזער קלוגשאַפֿט און קאָאָפּעראַציע מאַכן אונדזערע טאָקענס און אונדזער שכל די בעסטע וואָס עס איז פֿאַראַן — און יעדער מיטגליד דעפֿאַקטאָ שטאַרק רײַך. רײַך אין דער מטבע וואָס איז דאָ וויכטיק: באַוויזענער שכל וואַקסט צונויף ווי אַ ביבליאָטעק, ניט ווי אַ קוכן — יעדער צוגעלייגטער קערן מאַכט יעדן מיטגליד רײַכער אויף קיינעמס חשבון ניט, ביז אַ געוויינטלעכן מיטגליד'ס לאַפּע קאָמאַנדירט מער קאָנטראָלירבאַרע פֿעיִקייט ווי געלט קען דינגען.

פֿאַרוואָס די אַרבעט הייסט Wu

דער פֿאַבריק'ס אײנס פֿון אַרבעט — איין באַוויזענער כּלל, געשמידט פֿון אַ פּשוטן זאַץ — הייסט אַ Wu, לכּבֿוד Chien-Shiung Wu.

אין 1956 האָבן Chen-Ning Yang און Tsung-Dao Lee געפֿרעגט אַ גרויסאַרטיקע פֿראַגע — טוט די נאַטור מבֿדיל זײַן צווישן רעכטס און לינקס? — וואָס כּמעט יעדער האָט געמיינט איז ניט ווערט פֿרעגן. עס איז געווען Wu'ס עקספּערימענט — איר דיזײַן, איר אַפּאַראַט, איר מעסטונג — וואָס האָט עס געענטפֿערט. דער נאָבעל-פּרעמיע, דאָס קומענדיקע יאָר, איז אַוועק צו די טעאָרעטיקער אַליין. די פֿראַגע האָט פֿאַרדינט איר פּרעמיע; אַזוי אויך די ענטפֿער, און די ענטפֿער איז אַרויסגעלאָזט געוואָרן.

ביידע העלפֿטן פֿון יענער געשיכטע לעבן דאָ. די דרייסטע פֿראַגע, פּשוט געפֿרעגט, איז וווּ יעדער שטיק פֿון אונדזער אַרבעט הייבט זיך אָן — מיר כּבדן Yang, און מיר נעמען אים אַ בײַשפּיל. אָבער מיר רופֿן דעם אײנס פֿון אַרבעט לויט Wu, ווײַל דער באַווײַז איז די אַרבעט: ניט די אידעע, ניט די אָנזאָג — דער דעמאָנסטרירטער, קאָנטראָלירבאַרער רעזולטאַט. און מיר רופֿן עס לויט איר עפֿנטלעך, ווײַל מיר ווייסן ווי גרינג דער מענטש וואָס טוט דעם דעמאָנסטרירן ווערט אויסגעמעקט, און דאָס וועט דאָ ניט געשען.

וואָס קומט

• דער טערמינאַל — די לאַפּע וואָס די פֿאַרברייטערונגען דינען: אַן אָרטיקער אַסיסטענט אָן קיין צוהערער און אָן קיין אַרײַנוועג (ער פֿרעגט אַרויס; גאָרנישט קומט אַרײַן), און די באַשלוסים וואָס זענען וויכטיק, יעדער הינטער אַ באַוויזענעם קערן. אָפֿן-מקור (AGPL-3.0) — אַרויסגעגעבן: מקור-קאָד און בינערע פֿײַלן בײַ github.com/the-dark-factory/Ghillie_AGPL. קאָנטראָליר די בינערע פֿײַלן איידער דו לאָזט זיי לויפֿן: דער אַרויסגאָב טראָגט SHA256SUMS-assets.txt, וואָס דעקט די טאַרבאַלס פּונקט ווי אַראָפּגעלאָדן, אַזוי sha256sum -c SHA256SUMS-assets.txt קאָנטראָלירט זיי ווי זיי שטייען. (דער עלטערער SHA256SUMS איז נאָך דאָ פֿאַר וועמען עס האָט אים ציטירט; ער רעכנט אויף די קאָנטראָל-סומעס פֿון די אַנטפּאַקטע בינערע פֿײַלן אין אַ פּלאַטפֿאָרם-פּרעפֿיקסירטער פֿאָרם וואָס sha256sum -c קען ניט לייענען.)
• The catalogue is live — אַ לויפֿנדיקער ghillie אינסטאַלירט פֿאַרברייטערונגען וואָס לייטן זיך אַרויס אויף זײַן אייגענער מאַשין: ghillie -catalogue https://thereef.ink/catalogue -abilities-available, דערנאָך -get-ability <name> -reprove. גאָרנישט אינסטאַלירט זיך אַחוץ ווען זײַן באַווײַז לייט זיך אַרויס אויף דײַן הארדוועיר ערשט.
• The catalogue — מער אַרויסלייטבאַרע פֿאַרברייטערונגען אין דער זעלביקער פֿאָרם: שטילע שעהען, אויסגאָבע-סופֿיקן, קאָנטאַקט-דערלויבענישן, דער מויל-כּלל (אָפּווייזונגען ווערן קיינמאָל ניט איבערגעפֿראַזירט), יעדער מיט זײַנע טעאָרעמען גענעמט.
• The cooperative — געמיינזאַמע ליקנע-פּינקסים, אַזוי איין לאַפּעס פֿאַרשריבענער בלינדער פֿלעק ווערט יעדער לאַפּעס פֿאָראויזזעעניש, און צונויפֿגעלייגטע באַווײַז-אַרבעט: באַווײַזן איז דער איינציקער אַרבעטס-טייל וואָס מען קען זיכער אָננעמען פֿון פֿרעמדע, ווײַל אַן אַרויסלייטונג לייט זיך אָדער אַרויס אָדער ניט.

באַריכטן

האָסט אָנגעלאָפֿן דעם באַווײַז? צעבראָכן עפּעס העפֿלעך? געפֿונען דעם נודנעם רעזולטאַט? שרײַב צו tonythegair@gmail.com. געפֿינסן ווערן פּובליקירט; גאָרנישט מער וועגן דיר ווערט געבעטן — די בלאַט האָט קיין סקריפּטן ניט, קיין קיכלעך ניט, און קיין אַנאַליטיק ניט, וואָס דו קענסט נאָכקוקן דורך זי לייענען. די מאַשין וואָס גיט דיר איבער די בלאַט האַלט טאַקע איין קורצע, פֿאַרקירצטע שורה פֿאַר יעדער פֿאָדערונג, און זאָגט דאָס קלאָר: וואָס דער סערווער פֿאַרשרײַבט.

פּאַטראָנאַזש

TheReefink ווערט געפּאַטראָנירט דורך The Dark Factory Ltd, וואָס האָט געווידמעט באַטראַכטלעכע רעסורסן צו זײַן געלונגענקייט — די באַווײַז-מאַשינעריע, די ערשטע פֿאַרברייטערונגען, און דער קומענדיקער טערמינאַל. דער פּאַטראָנאַזש קויפֿט קיין אויסנאַמען ניט: אַלץ וואָס דער פּאַטראָן שיקט אַהער איז קאָנטראָלירבאַר לויט דעם זעלביקן כּלל ווי אַלץ אַנדערש, און אַ מיטגליד וואָס צעברעכט עס העפֿלעך האָט געטאָן דער גרופּע אַ טובֿה.