Deterministic Fixed Point Arithmetic | Dweve Numerus
Numerus: deterministic fixed-point, decimal and integer arithmetic in Rust; same bits under a declared execution contract. Publishing in round two.
Записът на случилото се, съхраняван, за да може да бъде прочетен отново.
SMT решавач, със сертификат, приложен към отговора.
Правила като именувани артефакти, с причината, поради която проверката е неуспешна.
Избери числовия договор преди първото изчисление, запази разсъжденията, които вървят с него, и дай на всеки, който попита, запис, който може да преизпълни на собствената си машина.
Това, което получавате, е сборът, изчислен точно, една и съща цифра навсякъде, и запис за това как е постигнат.
Изграден е в Европа, по европейски правила, и източникът му се публикува при условията на Apache-2.0 във втория кръг от програмата за основно публикуване на Dweve. Регулаторните органи и потребителските организации ще могат да проверят изчисленията директно, в деня, в който станат достъпни.
Дали дадено правило е справедливо, остава въпрос за хората, и вие имате право да го повдигнете. Това, което получавате, е нещо солидно, с което да го повдигнете: цифра, която излиза една и съща, когато някой я провери, писмен запис за това как е постигната, който не разчита на нечия памет, и проверка, която показва дали този запис е бил променен след това.
Ако правилото, което се прилага към вас, е несправедливо, това ще го приложи точно, до стотинка, за всеки, всеки път. То не прави правилото справедливо и не може да каже, че правилото е несправедливо. Всичко, което прави, е да гарантира, че цифрата не е грешна също, което е по-малко обещание, отколкото сте се надявали, и такова, което наистина се спазва.
Нищо от това не променя едното нещо, което трябва да чуете направо.
Така че до вас достига цифра с приложен към нея марж на грешка, или празно място там, където би стояло измислено число. Къде се намира машината също има значение, и то повече, отколкото хората очакват. Една и съща работа, извършена във Франция и в Германия, излиза с много различни въглеродни стойности, защото електричеството се произвежда по различен начин.
Броят не е съвършен и софтуерът го казва, без да бъде попитан. Задачи, твърде малки, за да бъдат регистрирани, не оставят никаква следа в него. Една и съща задача, изпълнена два пъти, се връща малко по-различна в зависимост от това колко е загряла машината. На някои наети компютри той не вижда нищо и го казва, вместо да гадае.
Компютрите използват електричество, за да мислят. Всеки знае това и никой никога не е успял да ви каже колко от него е отишло за която и да е задача. Процесорите водят собствен текущ отчет за енергията, която са изразходвали, и този отчет може да бъде прочетен. Така че една работа може да се върне с изписано до нея електричеството, което е отнело, а където машината не може да каже, с нищо, вместо с предположение.
То може също да отговори на нещо, което никой не би могъл да попита преди няколко години: колко струва сборът в електричество.
И нищо от това не трябва да се обажда някъде. Отчитането, дозата, спирачният път: цифрата се изчислява там, където се измерва, така че няма нейно копие на чужд компютър и нищо не чака връзка. Това има значение повече, когато числото е за тялото ви, отколкото когато е за водата ви.
Броителят е евтин отчасти защото изобщо не може да работи с дроби, затова брои в цели числа. Това се оказва същото броене, което дава идентичен отговор на всяка машина. Така че сборът във вашия шкаф не е по-груба версия на банковия сбор, защото кутията е малка. Той е същият сбор.
Броителят във вашия шкаф решава колко дължите за вода. Помпа в болнично отделение решава колко от лекарството да влезе. Кутия зад волана на кола решава колко силно да спре. Никой не ги наблюдава и всяка от тях прави същия вид аритметика, която банка прави с парите ви. Тя може да се направи до същия стандарт и отговорът никога не трябва да напуска стаята, в която е изчислен.
организация, която е запазила работещото, може да го предаде същия следобед
искате изчислението, а това е нормално нещо, което да поискате
и във всеки случай, изчислението, а не обобщение от него
публичен орган, за решение относно вашите пари
болница, за доза, която е била изчислена
доставчика на енергия, за сметка, която оспорвате
Направено по този начин, отговорът не е нечий спомен за случилото се. Числата, от които е започнало, са запазени, както и това, което е било направено с тях и в какъв ред. Пуснете го отново и излиза идентично, а не приблизително. Ако записът е бил променен междувременно, това се вижда първо, преди някой да пусне каквото и да е отново.
Вероятно сте го задали и сте получили лош отговор. Някой проверява текущата версия на изчислението, пуска я с днешните числа и ви казва, че излиза приблизително вярно. Никой не се измъква. Нещото, което е създало вашата цифра миналата пролет, вече не съществува, така че няма какво да посочите.
Нито едно от тези не отговаря на въпроса, който всеки би задал след това.
Миналата година излиза от новата система точно както е излизала от старата, така че декларацията, която сте подали, все още важи и няма следобед, който да загубите. Попитайте как е постигната дадена цифра и получавате изчислението, а не свиване на рамене. Не е нужно да вярвате на доверие, че изчислението не е било пипано, защото всичко, променено след това, се вижда.
Нито част от отговора не идва от машината. Няма закръгляне, което да върви по един начин на един чип и по друг на следващия, и няма пряк път, който по-бързият компютър да използва, а по-бавният да не използва. Сменете машината и цифрата не мърда, както и формулярът, който сте подали с нея, или писмото, което я е цитирало.
Някъде зад вашата банка, доставчика на енергия или данъчната служба софтуерът се сменя. Никой не ви казва и обикновено не ви пука. Пука ви в деня, в който новата система събере миналата година и получи различен отговор, защото формулярът, който вече сте подали, вече не съвпада със системата, която го е създала, и човекът, който трябва да обясни това, сте вие.
Сметка се урежда за седмица. Документите се препрочитат година по-късно.
Тук точката на закръгляне е записана веднъж, преди да се събере каквото и да е, и всяко копие на сметката ви следва нея. Така че няма телефонно обаждане, няма блокиране на сметката и няма три седмици. Копията съвпадат, защото са изчислени по един и същи начин, а не защото някой е седнал след това и ги е направил да съвпаднат.
Причината е по-малка, отколкото звучи. Данъкът излиза на части от цент и някой трябва да реши къде тези части се закръглят. Едната система закръгля на всеки ред. Другата закръгля веднъж, на общата сума. И двете са разумни и могат да се разминат с цент, без нито една от тях да греши.
Една сметка, три копия: касовият бон в ръката ви, касата на магазина и банката ви. От време на време две от тях завършват с различен цент. Нищо не е откраднато и никой не е небрежен, но пак вие поемате телефонното обаждане и вие чакате три седмици, докато някой реши кое копие е било вярно.
Достатъчно малко, за да го игнорирате, точно докато цифрата не е това, което дължите.
Това вместо това брои в цели числа, както бихте броили монети, така че нищо не остава и нищо не се отклонява. Това, което ви носи, е скучно и си струва. Телефонът ви, четецът на карти на щанда и компютър в друга държава всички завършват с една и съща цифра, а най-старото от трите не е по-малко вярно от най-новото.
Компютърът записва една десета така, както бихте записали една трета като десетична дроб, което означава не съвсем. Сама по себе си разликата е твърде малка, за да се види. Тя не остава сама: сметката има редове, годината има дванадесет сметки и всяка една от тези разлики все още стои в общата сума в долната част, която е цифрата, която ви молят да платите.
Цифрата, която са ви дали, е излязла от машина и различна машина може да ви е дала леко различна. Попитайте компютър за една десета плюс две десети и, ако го накарате да покаже всяка цифра, която държи, отговорът завършва със случайна четворка. Всяка машина прави това, така че никой не забелязва. Всяка една почиства случайната четворка по свой начин и така една сума, изчислена тук и изчислена в друга държава, завършва на две различни места.
Това, което получавате, е цифра, която отговаря сама за себе си, и решение за нея с дата.
Сертификационният пакет започва разговора с одитор, а това, което го приключва, е вашето подаване срещу собствения ви продукт, което никой не може да ви даде. И ако никоя цифра, която вашата организация произвежда, никога не трябва да бъде защитавана пред някой извън нея, честният отговор е, че нищо от това не си струва промяната.
Енергомерът обхваща една операционна система на една архитектура, а навсякъде другаде отказва, вместо да оценява. Доказването на свойство изисква външен решавател, инсталиран отделно, а без него получавате граници и интервали, които са полезни, но не са доказателства.
Нищо не го прави. Той произвежда доказателства, а човек оценява доказателствата. Той ще спазва лошо избран числов договор с пълна последователност и ще създаде безупречен запис за това, че го е направил, като записът е полезната част, а не обещание за коректност, защото обещанието не може да се провери, а записът може.