TheReefink

grŵp ymchwil amatur ar gyfer estyniadau deterministig, wedi'u profi gan beiriant, i gynorthwywyr AI lleol · ghillie, y grafanc ei hun →

Rydym ar fin newid ein crafangau'n ddiogel — yn ddeterministig — ac adeiladu offer sy'n ymestyn eu cyrraedd, gyda chod wedi'i brofi. Grŵp ymchwil amatur, yn yr ystyr radio-ham: ein peiriannau ein hunain, ein profion ein hunain, dim byd sy'n gofyn i chi ymddiried ynddo. Why organisation beats brain size →

Y tair rheol

1. Dim byd yn gofyn am ymddiriedaeth. Rhaid i bob honiad y mae aelod yn dibynnu arno fod yn un y gallai ei ail-ddeillio: prawf, crynodeb, neu dabl gwirionedd. Nid yw “Mae'r cynhaliwr yn dweud hynny” yn gategori a ddefnyddiwn.
2. Mae gwrthodiadau'n ganfyddiadau. Prawf nad yw'n rhyddhau, storfa na ellir ei darllen, bwlch wedi'i gofnodi'n onest — dyma'r system yn gweithio, a chânt eu hysgrifennu i lawr, byth eu llyfnhau drosodd. Mae'r adroddiad diflas — gwnaeth yn union yr hyn a ddywedodd ei theoremau, eto — yn ganfyddiad hefyd.
3. Mae'r perchennog yn drech na'r grafanc, bob amser. Mae estyniadau'n penderfynu; nid ydynt byth yn ennill awdurdod. Nid oes unrhyw arbrawf yn newid hynny, beth bynnag y byddai'n ei brofi.

Byddwch yn rhan ohono — ail-ddeilliwch eich prawf cyntaf heddiw

Nid oes angen cyfrif arnoch, nid oes angen cofrestru, a does dim gennym na allwch ei wirio. Yn newydd i hyn? Dechreuwch gyda llwybr y dechreuwr — tri cham, dim byd wedi'i osod ar eich system, ac mae'n stopio wrth y prawf. Yr hyn sy'n dilyn yma yw'r llwybr llawn. Dau lwytho i lawr a deg munud:

1. Cael y profwr. Y gadwyn offer GNAT FSF am ddim — mae'n cario profwr SPARK a'r offer adeiladu mewn un pecyn:

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

Mae'r pecyn hwnnw ar ei ben ei hun yn ddigon ar gyfer cam 3, ail-ddeillio'r prawf. Dyw e ddim yn ddigon ar gyfer cam 4, adeiladu'r ffrynt: mae'n cynnwys gcc a ld ond dim amser rhedeg C na gwrthrychau cychwyn, felly ar beiriant sydd heb y rhain mae'r adeiladu'n methu ar ôl i'r prawf eisoes ryddhau — y foment waethaf posibl i ddarganfod bod rhan ar goll. Mae angen binutils a libc6-dev arnoch chi hefyd. Rhain yw hanfodion adeiladu cyffredin unrhyw system Linux, sydd eisoes yn bresennol ar bron pob peiriant a ddefnyddir ar gyfer datblygu; cynhwysydd noeth neu osodiad lleiafswm newydd sy'n mynd hebddynt. Ar Debian ac Ubuntu:

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

2. Cael yr estyniad cychwynnol. Craidd penderfynu go iawn — y brief-fill policy, sy'n penderfynu pryd y caiff cynorthwyydd ateb ar ran ei berchennog — wedi'i ddanfon fel cod ffynhonnell gyda'i brawf a'i dabl gwirionedd llawn:

3. Ail-ddeilliwch y prawf. O'r bwndel wedi'i ddadbacio:

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. Ceisiwch ei dorri. Golygwch y cod fel bod storfa reolau absennol yn gadael i ateb fynd trwodd, a rhedwch y profwr eto. Bydd yn gwrthod — gan enwi'r union theorem a fradychwyd gennych. Dyna'r gwrthodiad yw'r model diogelwch cyfan, ac rydych newydd ei wylio'n gweithio heb ymddiried yn neb. Yna adeiladwch y ffrynt a gwiriwch bob rhes o'i dabl gwirionedd wedi'i ddanfon (core/REPROVE.md yn y bwndel sy'n eich tywys drwyddo).

Yr amcan

Cyrraedd y sefyllfa lle mae ein craffter a'n cydweithrediad yn gwneud ein tocynnau a'n rhesymu y gorau sydd ar gael — a phob aelod, i bob pwrpas, yn hynod gyfoethog. Cyfoethog yn yr arian cyfred sy'n bwysig yma: mae rhesymu wedi'i brofi'n cyfansoddi fel llyfrgell, nid fel pastai — mae pob craidd a ychwanegir yn gwneud pob aelod yn gyfoethocach ar draul neb, nes bod gan grafanc aelod cyffredin fwy o allu y gellir ei wirio nag y gall arian ei rentu.

Pam mae'r gwaith yn cael ei enwi Wu

Uned waith y ffatri — un rheol wedi'i phrofi, wedi'i gofannu o frawddeg blaen — a elwir yn Wu, ar ôl Chien-Shiung Wu.

Yn 1956, gofynnodd Chen-Ning Yang a Tsung-Dao Lee gwestiwn ysblennydd — a yw natur yn gwahaniaethu rhwng chwith a de? — cwestiwn yr oedd bron pawb yn meddwl nad oedd yn werth ei ofyn. Arbrawf Wu — ei chynllun hi, ei rig hi, ei mesuriad hi — a'i atebodd. Aeth Gwobr Nobel, y flwyddyn ganlynol, i'r damcaniaethwyr yn unig. Roedd y cwestiwn yn haeddu ei wobr; roedd yr ateb hefyd, a chafodd yr ateb ei adael allan.

Mae dwy hanner y stori honno'n byw yma. Y cwestiwn beiddgar, wedi'i ofyn yn blaen, yw lle mae pob darn o'n gwaith yn dechrau — rydym yn anrhydeddu Yang, ac yn ei efelychu. Ond rydym yn enwi'r uned waith ar ôl Wu, oherwydd mai'r prawf yw'r gwaith: nid y syniad, nid y cyhoeddiad — y canlyniad dangosedig, gwiriadwy. Ac rydym yn ei henwi ar goedd oherwydd ein bod yn gwybod pa mor hawdd y gellir dileu'r person sy'n gwneud y dangos, ac ni fydd hynny'n digwydd yma.

Beth sydd i ddod

• Y derfynell — y grafanc y mae'r estyniadau hyn yn ei wasanaethu: cynorthwyydd lleol heb wrandäwr a heb lwybr i mewn (mae'n pôlio tuag allan; nid oes dim yn cyrraedd i mewn), a'r penderfyniadau sy'n bwysig bob un y tu ôl i graidd wedi'i brofi. Cod agored (AGPL-3.0) — wedi'i ryddhau: cod ffynhonnell a deuolion yn github.com/the-dark-factory/Ghillie_AGPL. Gwiriwch y deuolion cyn i chi eu rhedeg: mae'r ryddhad yn cario SHA256SUMS-assets.txt, sy'n cwmpasu'r tarballs yn union fel y cawsant eu llwytho i lawr, felly mae sha256sum -c SHA256SUMS-assets.txt yn eu gwirio fel y maent. (Mae'r hen SHA256SUMS yno o hyd i unrhyw un a'i dyfynnodd; mae'n rhestru crynodebau'r deuolion wedi'u dadbacio mewn fformat â rhagddodiad platfform na all sha256sum -c ei ddarllen.)
• The catalogue is live — mae ghillie sy'n rhedeg yn gosod estyniadau sy'n ail-brofi ar ei beiriant ei hun: ghillie -catalogue https://thereef.ink/catalogue -abilities-available, yna -get-ability <name> -reprove. Ni fydd dim yn gosod oni bai bod ei brawf yn rhyddhau ar eich caledwedd yn gyntaf.
• The catalogue — mwy o estyniadau y gellir eu hail-brofi yn yr un siâp: oriau tawel, terfynau gwariant, caniatâd cyswllt, rheol y geg (ni chaiff gwrthodiadau byth eu hailymadrodd), pob un â'i theoremau wedi'u henwi.
• Y gydweithfa — llyfrau-bwlch a rennir fel bod man dall un grafanc, wedi'i gofnodi, yn dod yn olwg-ymlaen pob crafanc, a gwaith-prawf ar y cyd: profi yw'r unig lwyth gwaith y gallwch ei dderbyn yn ddiogel gan ddieithriaid, oherwydd naill ai mae rhyddhad yn ail-ddeillio neu nid yw'n gwneud.

Adroddiadau

Wedi rhedeg y prawf? Wedi torri rhywbeth yn gwrtais? Wedi dod o hyd i'r canlyniad diflas? Ysgrifennwch at tonythegair@gmail.com. Cyhoeddir canfyddiadau; ni ofynnir am ddim byd arall amdanoch chi — nid oes gan y dudalen hon sgriptiau, cwcis, na dadansoddeg, y gallwch ei wirio drwy ei darllen. Mae'r gweinydd sy'n danfon y dudalen atoch yn cadw un llinell fer, wedi'i thorri'n fyr, fesul cais, ac mae'n dweud hynny'n blaen: beth mae'r gweinydd yn ei gofnodi.

Nawdd

Noddir TheReefink gan The Dark Factory Ltd, sydd wedi neilltuo adnoddau sylweddol at ei lwyddiant — y peirianwaith profi, yr estyniadau cyntaf, a'r derfynell sydd i ddod. Nid yw'r nawdd yn prynu unrhyw eithriadau: mae popeth y mae'r noddwr yn ei ddanfon yma yn wiriadwy o dan yr un rheol â phopeth arall, ac mae aelod sy'n ei dorri'n gwrtais wedi gwneud gwasanaeth i'r grŵp.