TheReefink

buidheann rannsachaidh neo-dhreuchdail airson leudachaidhean cinntiche, air an dearbhadh le inneal, do luchd-cuideachaidh AI ionadail · ghillie, an spòg fhèin →

Tha sinn gu bhith ag atharrachadh nan spòg againn gu sàbhailte — gu cinntiche — agus a' togail innealan a leudaicheas an ruigheachd, le còd dearbhte. Buidheann rannsachaidh neo-dhreuchdail, san t-seagh radio-ham: na coimpiutairean againn fhèin, na dearbhaidhean againn fhèin, dad nach iarr ort earbsa a chur ann. Why organisation beats brain size →

An trì riaghailtean

1. Chan iarr dad earbsa. Feumaidh gach tagradh air a bheil ball an urra a bhith 'na fhear a b' urrainn dha ath-dhearbhadh: dearbhadh, geàrr-shamhla, no clàr fìrinn. Chan e “tha an neach-glèidhidh ag ràdh sin” roinn a chleachdas sinn.
2. Is e lorgan a th' ann an diùltaidhean. Dearbhadh nach coilean, tasgadan nach gabh leughadh, beàrn air a chlàradh gu h-onarach — is e seo an siostam ag obair, agus thèid an sgrìobhadh sìos, chan ann air an rèiteachadh a-mach. Tha an aithisg leibideach — rinn e dìreach na thuirt na teòiridhean aige, a-rithist — 'na lorg cuideachd.
3. Tha an sealbhadair os cionn na spòig, an-còmhnaidh. Bidh leudachaidhean a' co-dhùnadh; cha chosnaich iad ùghdarras a-riamh. Chan atharraich deuchainn sam bith sin, ge b' e dè a dhearbhadh e.

Bi 'nad phàirt dheth — ath-dhearbh a' chiad dhearbhadh agad an-diugh

Chan eil feum agad air cunntas, chan eil feum agad air clàradh, agus chan eil dad againn nach urrainn dhut sgrùdadh. Ùr dhan seo? Tòisich le slighe an neach-tòiseachaidh — trì ceumannan, dad air a stàladh air an t-siostam agad, agus stadaidh e aig an dearbhadh. Is e seo an t-slighe làn a leanas. Dà luchdachadh a-nuas agus deich mionaidean:

1. Faigh an dearbhaiche. An sreath-inneal GNAT FSF an asgaidh — tha e a' giùlan dearbhaiche SPARK agus na h-innealan togail ann an aon phasgan:

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

Tha am pasgan sin leis fhèin gu leòr airson ceum 3, ath-dhearbhadh an dearbhaidh. Chan eil e gu leòr airson ceum 4, togail a' bheòil: tha e a' giùlan gcc agus ld ach gun àm-ruith C agus gun nithean tòiseachaidh, agus mar sin air coimpiutair aig nach eil iad sin, fàilligidh an togail às dèidh don dearbhadh a bhith air coileanadh mu thràth — an dòigh as miosa a b' urrainnear pìos a lorg a dhìth. Feumaidh tu binutils agus libc6-dev cuideachd. Is iad seo prìomh riatanasan togail cumanta siostam Linux sam bith, a tha an làthair mu thràth air cha mhòr a h-uile coimpiutair a chleachdar airson leasachaidh; is e soitheach lom no stàladh lugha ùr aig nach eil iad. Air Debian agus Ubuntu:

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

2. Faigh an leudachadh tòiseachaidh. Cridhe co-dhùnaidh fìor — am brief-fill policy, a' co-dhùnadh cuin as urrainn do luchd-cuideachaidh freagairt a thoirt seachad às leth an sealbhadair — air a lìbhrigeadh mar chòd tùsail le a dhearbhadh agus a chlàr fìrinn slàn:

3. Ath-dhearbh an dearbhadh. Bhon phasgan neo-phacaichte:

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. Feuch ri a bhriseadh. Deasaich an còd gus an leig tasgadan riaghailtean a dhìth freagairt troimhe, agus ruith an dearbhaiche a-rithist. Diùltaidh e — ag ainmeachadh an teòirim mionaideach a bhrath thu. Is e an diùltadh sin am modail tèarainteachd gu lèir, agus tha thu dìreach air fhaicinn ag obair gun earbsa a chur an duine sam bith. An uairsin tog am beul agus sgrùd gach sreath den chlàr fhìrinn a chuir e a-mach (core/REPROVE.md anns a' phasgan gad threòrachadh troimhe).

An t-amas

Ruighinn an t-suidheachadh far a bheil ar geurad agus ar co-obrachadh a' dèanamh nan tòcanan againn agus ar reusanachadh as fheàrr a tha ri fhaighinn — agus gach ball, gu practaigeach, sàr-bheairteach. Beairteach san airgead-cùbhrainn a tha cudromach an seo: tha reusanachadh dearbhte a' cur-ri-chèile mar leabharlann, chan ann mar phìos — bidh gach cridhe a chuirear ris a' dèanamh gach ball nas beairtiche air cosgais duine sam bith, gus am bi barrachd comas a ghabhas sgrùdadh aig spòg ball àbhaisteach na dh'fhaodas airgead a mhàl.

Carson a tha an obair air ainmeachadh Wu

Is e Wu, air ainmeachadh airson Chien-Shiung Wu, aonad-obrach an fhactaraidh — aon riaghailt dhearbhte, air a gobhainneachd bho sheantans shìmplidh.

Ann an 1956, dh'fhaighnich Chen-Ning Yang agus Tsung-Dao Lee ceist mhòrail — an innis nàdar eadar deas is clì? — ceist nach robh cha mhòr duine sam bith den bheachd a b' fhiach fhaighneachd. B' e deuchainn Wu — a dealbhadh fhèin, a h-uidheam fhèin, an tomhas aice fhèin — a fhreagair i. Chaidh Duais Nobel, an ath-bhliadhna, chun luchd-teòiridh a-mhàin. Bha an ceist airidh air a duais; bha am freagairt cuideachd, agus chaidh am freagairt fhàgail a-mach.

Tha an dà leth den sgeulachd sin beò an seo. Is e a' cheist dhàna, air a faighneachd gu soilleir, far an tòisicheas gach pìos den obair againn — tha sinn a' toirt urram do Yang, agus 'ga aithris. Ach tha sinn ag ainmeachadh aonad na h-obrach às dèidh Wu, oir is e an dearbhadh an obair: chan e am beachd, chan e am foillseachadh — an toradh air a nochdadh, a ghabhas sgrùdadh. Agus tha sinn ga h-ainmeachadh gu poblach oir tha fios againn cho furasta 's a thèid an neach a rinn an nochdadh a dhubhadh às, agus cha tachair sin an seo.

Na tha ri thighinn

• An t-eangarra — an spòg a tha na leudachaidhean seo a' frithealadh: luchd-cuideachaidh ionadail gun èisdear agus gun shlighe a-steach (bidh e a' cnagadh a-mach; cha ruig dad a-steach), agus na co-dhùnaidhean cudromach gach fear air cùl cridhe dhearbhte. Còd fosgailte (AGPL-3.0) — air a leigeil ma sgaoil: còd tùsail agus dà-fhillte aig github.com/the-dark-factory/Ghillie_AGPL. Sgrùd na dà-fhillte mus ruith thu iad: tha an sgaoileadh a' giùlan SHA256SUMS-assets.txt, a tha a' còmhdach nan tarballs dìreach mar a fhuaireadh iad, agus mar sin bidh sha256sum -c SHA256SUMS-assets.txt gan sgrùdadh mar a tha iad. (Tha an seann SHA256SUMS ann fhathast do dhuine sam bith a thug iomradh air; tha e a' liostadh geàrr-shamhlaidhean nan dà-fhillte neo-phacaichte ann an cruth le ro-leasachan àrd-ùrlair nach gabh sha256sum -c a leughadh.)
• The catalogue is live — bidh ghillie a tha a' ruith a' stàladh leudachaidhean a dh'ath-dhearbhas air a choimpiutair fhèin: ghillie -catalogue https://thereef.ink/catalogue -abilities-available, an uairsin -get-ability <name> -reprove. Cha stàlaich dad mura h-eil an dearbhadh aige a' coileanadh air an t-àbhaist-chruaidh agad an toiseach.
• The catalogue — barrachd leudachaidhean a ghabhas ath-dhearbhadh san aon chruth: uairean sàmhach, mullaichean caitheimh, tabhartasan conaltraidh, riaghailt a' bheòil (chan ath- sgrìobhar diùltaidhean a-riamh), gach fear le a theòiridhean air an ainmeachadh.
• An co-obrachail — leabhraichean-beàrn a tha air an co-roinn gus am bi ball dall aon spòig, air a chlàradh, 'na ro-shealladh aig gach spòg, agus obair-dhearbhaidh còmhla: is e dearbhadh an aon eallach obrach a ghabhas tu gu sàbhailte bho choigrich, oir an dàrna cuid tha sgaoileadh ag ath-dhearbhadh no chan eil.

Aithisgean

An do ruith thu an dearbhadh? An do bhris thu rud gu modhail? An do lorg thu an toradh leibideach? Sgrìobh gu tonythegair@gmail.com. Thèid lorgan fhoillseachadh; chan iarrar càil eile mud dheidhinn — chan eil sgriobtaichean, briosgaidean, no anailis aig an duilleag seo, a ghabhas sgrùdadh le bhith ga leughadh. Bidh am frithealaiche a lìbhrigeas an duilleag dhut a' cumail aon loidhne ghoirid, ghearraichte, gach iarrtas, agus tha e ag ràdh sin gu soilleir: na chlàraicheas am frithealaiche.

Taic

Tha taic aig TheReefink bho The Dark Factory Ltd, a thug seachad goireasan mòra airson a shoirbheachaidh — an innealradh dearbhaidh, a' chiad leudachaidhean, agus an t-eangarra a tha ri thighinn. Cha cheannaich an taic sin cead sam bith: tha a h-uile càil a chuireas an neach-taice a-mach an seo sgrùdte fon aon riaghailt ri gach càil eile, agus tha ball a bhriseas i gu modhail air seirbheis a dhèanamh don bhuidheann.