Zauważyłem, że o wiele łatwiej jest mi zapisać matematyczne dowody bez popełniania błędów niż napisać program komputerowy bez błędów.

Wydaje się, że jest to coś bardziej rozpowszechnionego niż tylko moje doświadczenie. Większość ludzi cały czas popełniają błędy w oprogramowaniu i mają kompilator, który cały czas mówi im, jaki jest błąd. Nigdy nie słyszałem o kimś, kto napisał duży program komputerowy bez pomyłek za jednym razem i miał pełną pewność, że będzie bezbłędny. (W rzeczywistości prawie żaden program nie jest bezbłędny, nawet wiele z nich jest bardzo debugowanych).

Jednak ludzie mogą pisać całe dokumenty lub książki z dowodami matematycznymi bez kompilatora, który nigdy nie przekaże opinii, że popełnił błąd, a czasem nawet nie otrzyma opinii od innych.

Pozwól mi wyjaśnić. nie oznacza to, że ludzie nie popełniają błędów w dowodach matematycznych, ale dla nawet średnio doświadczonych matematyków błędy zwykle nie są tak problematyczne i można je rozwiązać bez pomocy jakiejś „zewnętrznej wyroczni”, takiej jak kompilator wskazujący na twój błąd.

W rzeczywistości, gdyby tak nie było, to matematyka prawie nie byłaby możliwa, jak mi się wydaje.

To skłoniło mnie do zadania pytania: co takiego różni się od pisania bezbłędnych dowodów matematycznych i pisania nienagannego kodu komputerowego, co sprawia, że ​​ten pierwszy jest o wiele łatwiejszy do opanowania niż drugi?

Można powiedzieć, że po prostu fakt, że ludzie mają „zewnętrzną wyrocznię” kompilatora wskazującą im na swoje błędy, sprawia, że ​​programiści są leniwi, uniemożliwiając im robienie tego, co niezbędne do rygorystycznego pisania kodu. Ten pogląd oznaczałby, że gdyby nie mieli kompilatora, byliby równie bezbłędni jak matematyki.

Może się to wydawać przekonywujące, ale w oparciu o moje doświadczenie programowania i spisywania matematycznych dowodów intuicyjnie wydaje mi się, że to naprawdę nie jest wyjaśnienie. Wydaje się, że w tych dwóch przedsięwzięciach jest coś bardziej fundamentalnie innego.

Moją początkową myślą jest to, że różnica może być taka, że ​​dla matematyka poprawny dowód wymaga poprawności każdego logicznego kroku. Jeśli każdy krok jest prawidłowy, cały dowód jest poprawny. Z drugiej strony, aby program był bezbłędny, nie tylko każda linia kodu musi być poprawna, ale musi również działać jej związek z każdą inną linią kodu w programie.

Innymi słowy, jeśli krok w dowodzie jest poprawna, to popełnia błąd w kroku Y nie będzie bałagan krok kiedykolwiek. Ale jeśli wiersz kodu zostanie poprawnie zapisany, to popełnienie błędu w wierszu wpłynie na działanie wiersza , dlatego za każdym razem, gdy piszemy wiersz musimy brać pod uwagę jego stosunek do wszystkich innych wierszy. Możemy użyć enkapsulacji i wszystkich tych rzeczy, aby to ograniczyć, ale nie można jej całkowicie usunąć.$X$$Y$X Y X $X$$X$$Y$$X$$X$

Oznacza to, że procedura sprawdzania błędów w dowodzie matematycznym jest zasadniczo liniowa pod względem liczby kroków sprawdzających, ale procedura sprawdzania błędów w kodzie komputerowym jest zasadniczo wykładnicza pod względem liczby wierszy kodu.

Co myślisz?

Uwaga: To pytanie zawiera wiele odpowiedzi, które eksplorują różnorodne fakty i punkty widzenia. Zanim odpowiesz, przeczytaj je wszystkie i odpowiedz tylko, jeśli masz coś nowego do dodania. Zbędne odpowiedzi lub odpowiedzi, które nie wspierają opinii faktami, mogą zostać usunięte.

Pozwól, że podam jeden powód i jedno nieporozumienie jako odpowiedź na twoje pytanie.

Głównym powodem , że łatwiej jest napisać (pozornie) prawidłowych dowodów matematycznych jest to, że są one napisane na bardzo wysokim poziomie. Załóżmy, że możesz napisać taki program:

function MaximumWindow(A, n, w):
    using a sliding window, calculate (in O(n)) the sums of all length-w windows
    return the maximum sum (be smart and use only O(1) memory)

O wiele trudniej byłoby pomylić się podczas programowania w ten sposób, ponieważ specyfikacja programu jest znacznie bardziej zwięzła niż jego implementacja . Rzeczywiście, każdy programista, który próbuje przekonwertować pseudokod na kod, a zwłaszcza na kod efektywny, napotyka dużą przepaść między ideą algorytmu a szczegółami jego implementacji . Dowody matematyczne koncentrują się bardziej na pomysłach, a mniej na szczegółach.

Prawdziwym odpowiednikiem kodu dla dowodów matematycznych są dowody wspierane komputerowo . Są one znacznie trudniejsze do opracowania niż zwykłe dowody tekstowe i często odkrywa się różne ukryte rogi, które są „oczywiste” dla czytelnika (który zwykle nawet ich nie zauważa), ale nie tak oczywiste dla komputera. Ponadto, ponieważ komputer może obecnie wypełnić tylko stosunkowo niewielkie luki, dowody muszą zostać opracowane do takiego poziomu, aby czytający je człowiek nie trafił w las za drzewa.

Ważnym nieporozumieniem jest to, że matematyczne dowody są często poprawne. W rzeczywistości jest to raczej optymistyczne. Bardzo trudno jest pisać skomplikowane dowody bez błędów, a dokumenty często zawierają błędy. Być może najbardziej znanymi ostatnimi przypadkami są pierwsza próba Wilesa (szczególny przypadek) twierdzenia o modułowości (co implikuje ostatnie twierdzenie Fermata) oraz różne luki w klasyfikacji skończonych prostych grup, w tym ponad 1000 stron o grupach quasithin, które były napisane 20 lat po rzekomym zakończeniu klasyfikacji.

Pomyłka w papierze Voevodsky uczynił go wątpliwości pisemne dowody tyle, że zaczął opracowanie teorii typów homotopii , logiczne ramy przydatnych do opracowania teorii homotopy formalnie, i od tej pory korzystały z komputera, aby sprawdzić wszystkie jego późniejsze prace (przynajmniej według własnego wstęp). Chociaż jest to skrajna (i obecnie niepraktyczna) pozycja, nadal zdarza się, że korzystając z wyniku, należy przejrzeć dowód i sprawdzić, czy jest poprawny. W mojej okolicy znajduje się kilka artykułów, o których wiadomo, że są błędne, ale nigdy nie zostały wycofane, a ich status przekazywany jest ekspertom od ust do ucha.

(Prawdopodobnie ryzykuję tutaj kilka głosów negatywnych, ponieważ nie mam czasu / zainteresowania, aby udzielić właściwej odpowiedzi, ale uważam, że cytowany tekst (i resztę cytowanego artykułu poniżej) jest dość wnikliwy, biorąc również pod uwagę, że są napisane przez znanego matematyka. Być może mogę poprawić odpowiedź później.)

Pomysł, który, jak przypuszczam, nie różni się szczególnie od istniejącej odpowiedzi, jest taki, że „dowód” lub argument przekazuje się matematycznej społeczności, której celem jest przekonanie ich, że (żmudne) szczegóły można w zasadzie wypełnić aby uzyskać w pełni określony formalny dowód - bez robienia tego często. Jednym z krytycznych przykładów tego jest to, że można wykorzystać istniejące twierdzenia, po prostu je przedstawiając, ale ponowne użycie kodu jest ogólnie znacznie trudniejsze. Weź również pod uwagę drobne „błędy”, które mogą całkowicie pozbawić fragment kodu (np. SEGFAULT), ale mogą pozostawić matematyczny argument w dużej mierze nienaruszony (to znaczy, jeśli błąd może zostać zawarty bez zwijania się argumentu).

Standard poprawności i kompletności niezbędny do uruchomienia programu komputerowego jest o kilka rzędów wielkości wyższy niż standard obowiązujących dowodów matematycznych. Niemniej jednak duże programy komputerowe, nawet jeśli zostały bardzo starannie napisane i bardzo dokładnie przetestowane, zawsze zawierają błędy. [...] Matematyka, którą ćwiczymy, jest o wiele bardziej formalnie kompletna i precyzyjna niż inne nauki, ale pod względem treści jest znacznie mniej formalnie i precyzyjna niż programy komputerowe. Różnica dotyczy nie tylko wysiłku: rodzaj wysiłku jest jakościowo różny. W dużych programach komputerowych ogromną część wysiłku należy poświęcić niezliczonym problemom ze zgodnością: upewniając się, że wszystkie definicje są spójne, rozwijając „dobre” struktury danych, które mają użyteczną, ale nie uciążliwą ogólność, decydującą o „właściwej” ogólności dla funkcji itp. Udział energii wydatkowanej na część roboczą dużego programu, w odróżnieniu od części księgowej, jest zaskakująco mały. Ze względu na problemy ze zgodnością, które niemal nieuchronnie wymykają się spod kontroli, ponieważ „właściwe” definicje zmieniają się wraz z dodawaniem ogólności i funkcjonalności, programy komputerowe zwykle wymagają częstego przepisywania, często od zera.

O dowodzie i postępach w matematyce (s. 9-10), autor: WILLIAM P. THURSTON https://arxiv.org/pdf/math/9404236.pdf

Pozwólcie, że zacznę od cytowania EW Dijkstry:

„Programowanie jest jedną z najtrudniejszych gałęzi matematyki stosowanej; biedniejsi matematycy powinni pozostać czystymi matematykami”. (od EWD498)

Chociaż to, co Dijkstra miał na myśli przez `` programowanie '' różni się nieco od obecnego użycia, w tym cytacie wciąż jest pewna wartość. Inne odpowiedzi wspominały już, że poziom abstrakcji w matematyce może być znacznie wyższy niż w programowaniu, co oznacza, że ​​możemy zignorować pewne trudne fragmenty, jeśli chcemy to zrobić.

Uważam jednak, że jest to jedynie konsekwencja bardziej fundamentalnej różnicy między dowodem a programem komputerowym, co jest ich celem .

Głównym celem dowodu matematycznego jest między innymi przekonanie się, że twierdzenie matematyczne jest poprawne, a może nawet ważniejsze - osiągnięcie zrozumienia . Dlatego możesz pracować tylko w świecie matematyki, w którym wszystko jest stworzone w taki sposób, że zrozumienie można osiągnąć poprzez projektowanie (chociaż niektórzy uczniowie zaczynają się różnić ...) Właśnie to Dijkstra miał na myśli z „czystymi matematykami”, tymi, którzy (prawie) dotyczą wyłącznie faktów matematycznych i zrozumienia ich właściwości.

Nie należy się zatem dziwić, że poprawne proofy są względnie odporne na błędy: to jest sedno całego „ćwiczenia”. (Mimo to nie oznacza to, że błędy nie istnieją lub ledwo istnieją, ponieważ błąd jest tylko ludzki, mówią)

Jeśli więc rozważymy programowanie, jaki jest nasz cel? Tak naprawdę nie szukamy zrozumienia, chcemy czegoś, co działa . Ale kiedy coś „działa”? Coś działa, gdy udało nam się stworzyć coś, co pozwala jakiejś dziwnej maszynie na wykonanie zadania, które chcemy, a najlepiej dość szybko.

Jest to, moim zdaniem, podstawowa różnica, ponieważ oznacza, że ​​nasz cel nie może być po prostu określony jako jakieś twierdzenie, które nasz program „dowodzi”, pragniemy czegoś w świecie rzeczywistym (cokolwiek to jest), a nie jakiegoś artefaktu matematycznego. Oznacza to, że nie możemy czysto teoretycznie osiągnąć naszego celu (chociaż Dijkstra chciałby, abyś spróbował go niezależnie od tego), ponieważ musimy uspokoić maszynę, mieć nadzieję, że faktycznie wiemy, jakie zadanie chcemy wykonać, a także jesteśmy świadomi rzeczy, których jeszcze nie wziąłem pod uwagę jakoś.

Tak więc ostatecznie nie ma innego wyjścia, jak tylko wypróbować i prawdopodobnie zawieść, naprawić, zawieść i spróbować ponownie, dopóki nie będziemy w pewnym stopniu zadowoleni z wyniku.

Zauważ, że twoja hipoteza pisania bezbłędnych dowodów jest prostsza niż bezbłędne programy (które w rzeczywistości są różnymi stwierdzeniami, jak wskazuje @Ariel ) mogą być w rzeczywistości błędne, ponieważ dowody są często konstruowane metodą prób i błędów na pewnym poziomie. Mam jednak nadzieję, że rzuci to nieco światła na postawione pytanie: „Jaka jest naprawdę różnica między udowodnieniem jakiegoś twierdzenia a napisaniem programu?” (Do którego nieostrożny obserwator korespondencji Curry-Howarda może powiedzieć: „W ogóle nic!”)

Jak wspomniano w komentarzach @wvxvw, bardzo istotne są następujące akapity z „uwag na temat programowania strukturalnego” (EWD249, strona 21):

(...) Program sam w sobie nigdy nie jest celem; celem programu jest wywołanie obliczeń, a celem obliczeń jest uzyskanie pożądanego efektu. Chociaż program jest produktem końcowym wykonanym przez programistę, możliwe wywołane przez niego obliczenia - których „wykonanie” pozostawia się maszynie! - są prawdziwym przedmiotem jego handlu. Na przykład, gdy programiści stwierdzą, że jego program jest poprawny, naprawdę wypowiada się na temat obliczeń, które może wywołać.

(...) W pewnym sensie tworzenie programu jest zatem trudniejsze niż tworzenie teorii matematycznej: zarówno program, jak i teoria są uporządkowanymi, ponadczasowymi obiektami. Ale chociaż teoria matematyczna ma sens w obecnej formie, program ma sens tylko poprzez jej wykonanie.

Lamport daje podstawy do sporu na temat występowania błędów w dowodach w Jak napisać dowód (strony 8-9) :

Jakieś dwadzieścia lat temu postanowiłem napisać dowód twierdzenia Schroedera-Bernsteina dla wstępnej klasy matematyki. Najprostszym dowodem, jaki mogłem znaleźć, był klasyczny tekst ogólnej topologii Kelleya. Ponieważ Kelley pisał dla bardziej wyrafinowanej publiczności, musiałem dołożyć wiele wyjaśnień do jego półstronicowego dowodu. Napisałem pięć stron, kiedy zdałem sobie sprawę, że dowód Kelleya był błędny. Ostatnio chciałem zilustrować wykład na temat mojego stylu dowodu przekonującym błędnym dowodem, więc zwróciłem się do Kelleya. Nie mogłem znaleźć nic złego w jego dowodzie; wydawało się to oczywiście poprawne! Czytanie i ponowne odczytanie dowodu przekonało mnie, że albo moja pamięć zawiodła, albo dwadzieścia lat temu byłem bardzo głupi. Mimo to dowód Kelleya był krótki i stanowiłby dobry przykład, więc zacząłem przepisywać go jako dowód strukturalny.

... Styl został po raz pierwszy zastosowany do dowodów zwykłych twierdzeń w artykule, który napisałem z Martinem Abadi. Napisał już konwencjonalne dowody - dowody, które były na tyle dobre, by przekonać nas i przypuszczalnie sędziów. Przepisując dowody w ustrukturyzowanym stylu, odkryliśmy, że prawie każdy miał poważne błędy, chociaż twierdzenia były prawidłowe. Wszelkie nadzieje, że nieprawidłowe dowody nie doprowadzą do błędnych twierdzeń, zostały zniszczone podczas naszej następnej współpracy. Raz po raz robiliśmy przypuszczenia i piszemy na tablicy szkic dowodowy - szkic, który można łatwo przekształcić w przekonujący konwencjonalny dowód - tylko po to, aby odkryć, próbując napisać ustrukturyzowany dowód, że domniemanie jest fałszywe. Od tego czasu nigdy nie wierzyłem w wynik bez dokładnego, ustrukturyzowanego dowodu.

Jedną dużą różnicą jest to, że programy są zwykle pisane do działania na danych wejściowych, podczas gdy matematyczne dowody zwykle zaczynają się od zestawu aksjomatów i wcześniej znanych twierdzeń. Czasami trzeba objąć wiele spraw narożnych, aby uzyskać wystarczająco ogólny dowód, ale sprawy i ich rozstrzygnięcie jest wyraźnie wymienione, a zakres wyniku jest domyślnie ograniczony do tych spraw.

Porównaj to z programem komputerowym, który musi zapewniać „prawidłowe” wyjście dla szeregu możliwych wejść. Rzadko można wyliczyć wszystkie dane wejściowe i wypróbować je wszystkie. Co gorsza, załóżmy, że program współdziała z człowiekiem i pozwala jego wkładowi modyfikować funkcjonowanie? Ludzie są niezwykle nieprzewidywalni, a liczba możliwych danych wejściowych do rozsądnie dużego programu z ludzkimi interakcjami rośnie w zadziwiającym tempie. Musisz spróbować przewidzieć różne sposoby używania programu i spróbować sprawić, aby wszystkie przypadki użycia działały lub przynajmniej kończyły się niepowodzeniem w rozsądny sposób, gdy niepowodzenie jest jedyną opcją. I zakładając, że wiesz, jak to powinno działać we wszystkich tych niejasnych narożnych skrzyniach.

Wreszcie dużego programu nie można tak naprawdę porównać do pojedynczego dowodu, nawet złożonego. Duży program jest prawdopodobnie bardziej podobny do gromadzenia i recenzowania małej biblioteki literatury, z których niektóre mogą zawierać błędy, które należy obejść. W przypadku programów bardziej w skali pojedynczego dowodu, który może być małą implementacją algorytmu, powiedzmy, doświadczeni inżynierowie oprogramowania mogą wykonać je bez popełniania błędów, szczególnie przy użyciu nowoczesnych narzędzi, które zapobiegają / rozwiązują typowe trywialne błędy (takie jak błędy ortograficzne) ), które są równoważne z wczesnymi problemami, które można rozwiązać podczas korekty.

Mówią, że problem z komputerami polega na tym, że tak robią dokładnie to , co im powiesz.

Myślę, że może to być jeden z wielu powodów.

Zauważ, że w programie komputerowym pisarz (ty) jest inteligentny, ale czytnik (CPU) jest głupi.
Ale z matematycznym dowodem pisarz (ty) jest inteligentny, a czytelnik (recenzent) jest również inteligentny.

Oznacza to, że nigdy nie możesz sobie pozwolić na „cóż, wiesz o co mi chodzi sytuację „z komputerem ”. Robi dokładnie to, co mówisz, nie znając swoich intencji.

Powiedzmy, że jest to krok w pewnym dowodzie:

$x^2+4x+3$$x+3$$x = -3$

Jednym z problemów, który moim zdaniem nie został rozwiązany w odpowiedzi Yuvala, jest to, że porównujesz różne zwierzęta.

$n$$n!$

Weryfikacja właściwości semantycznych programów jest nierozstrzygalna (twierdzenie Rice'a) i analogicznie, sprawdzenie, czy instrukcja w logice predykatów pierwszego rzędu jest prawdziwa, jest również nierozstrzygalna. Chodzi o to, że nie ma prawdziwej różnicy w twardości od sposobu patrzenia na problemy. Z drugiej strony możemy argumentować o właściwościach syntaktycznych programów (kompilatorów), co jest analogiczne do faktu, że możemy weryfikować dowody. Błędy (kod nie robi tego, co chcę) są semantyczne, więc powinieneś porównać je z ich poprawnym odpowiednikiem.

Umocnię Yuvala i powiem, że całe pola rosły dzięki motywacji do pisania matematycznych dowodów, które można zapisać i zweryfikować w jakimś formalnym systemie, więc nawet proces weryfikacji wcale nie jest trywialny.

Co takiego różni się w pisaniu bezbłędnych dowodów matematycznych i pisaniu bezbłędnego kodu komputerowego, który sprawia, że ​​ten pierwszy jest o wiele łatwiejszy do opanowania niż drugi?

Uważam, że podstawowymi przyczynami są idempotencja (daje te same wyniki dla tych samych danych wejściowych) i niezmienność (nie zmienia się).

Co jeśli dowód matematyczny mógłby dać inne wyniki, gdyby został odczytany we wtorek lub gdy rok przekroczył 2000 r. Od 1999 r.? Co jeśli częścią matematycznego dowodu było cofnięcie się o kilka stron, ponowne napisanie kilku wierszy, a następnie rozpoczęcie od nowa od tego momentu?

Jestem pewien, że taki dowód byłby prawie tak podatny na błędy jak normalny segment kodu komputerowego.

Widzę także inne czynniki wtórne:

1. Matematycy są zwykle znacznie lepiej wykształceni przed próbą napisania znaczącego / możliwego do opublikowania dowodu. 1/4 samodzielnych programistów zaczęło kodować mniej niż 6 lat temu (patrz badanie SO 2017 ), ale zakładam, że większość matematyków ma ponad dekadę formalnej edukacji matematycznej.
2. Dowody matematyczne rzadko są trzymane na tym samym poziomie kontroli, co kod komputerowy. Jedna literówka może zniszczyć program, ale dziesiątki literówek mogą nie wystarczyć do zniszczenia wartości dowodu (tylko jego czytelności).
3. Diabeł tkwi w szczegółach, a kod komputerowy nie może pominąć szczegółów. Dowody mogą pomijać kroki, które są uważane za proste / rutynowe. Istnieje kilka miłych cukrów składniowych dostępnych we współczesnych językach, ale są one mocno zakodowane i dość ograniczone w porównaniu.
4. Matematyka jest starsza i ma bardziej solidny fundament / rdzeń. Z pewnością istnieje mnóstwo nowych i błyszczących pól matematycznych, ale większość podstawowych zasad jest stosowana od dziesięcioleci. To prowadzi do stabilności. Z drugiej strony programiści nadal nie zgadzają się na podstawową metodologię kodowania (wystarczy zapytać o rozwój Agile i jego szybkość adopcji).

Zgadzam się z tym, co napisał Yuval. Ale mają też o wiele prostszą odpowiedź: w praktyce inżynierowie oprogramowania zazwyczaj nie próbują nawet sprawdzić poprawności swoich programów, po prostu tego nie robią, zwykle nawet nie zapisują warunków, które określają, kiedy program jest poprawny.

Są tego różne przyczyny. Jednym z nich jest to, że większość inżynierów oprogramowania nie ma umiejętności jasnego matematycznego formułowania problemów ani nie wie, jak pisać dowody poprawności.

Kolejnym jest to, że zdefiniowanie warunków poprawności dla złożonego systemu oprogramowania (szczególnie rozproszonego) jest bardzo trudnym i czasochłonnym zadaniem. Oczekuje się, że będą mieli coś, co wydaje się działać w ciągu kilku tygodni.

Innym powodem jest to, że poprawność programu zależy od wielu innych systemów napisanych przez inne, które znowu nie mają wyraźnej semantyki. Istnieje prawo Hyrum, które zasadniczo mówi, że jeśli twoja biblioteka / usługa ma możliwe do zaobserwowania zachowanie (nie jest częścią umowy), ktoś w końcu będzie od niej zależał. Zasadniczo oznacza to, że pomysł tworzenia oprogramowania w formie modułowej z wyraźnymi umowami, takimi jak lematy w matematyce, nie działa w praktyce. Gorzej jest w językach, w których stosuje się odbicie. Nawet jeśli program jest dzisiaj poprawny, jutro może się zepsuć, gdy ktoś przeprowadzi jakieś trywialne refaktoryzowanie w jednej z jego zależności.

W praktyce zwykle dzieje się tak, że mają testy. Testy działają zgodnie z oczekiwaniami programu. Za każdym razem, gdy zostanie znaleziony nowy błąd, dodają testy, aby go złapać. Działa do pewnego stopnia, ale nie jest to dowód poprawności.

Kiedy ludzie nie mają umiejętności definiowania poprawności ani pisania poprawnych programów, ani nie są tego zobowiązani, a robienie tego jest raczej trudne, nie jest zaskoczeniem, że oprogramowanie nie jest poprawne.

Należy jednak pamiętać, że na końcu w lepszych miejscach inżynieria oprogramowania odbywa się poprzez przegląd kodu. To znaczy, że autor programu musi przekonać co najmniej jedną inną osobę, że program działa poprawnie. W tym miejscu powstają nieformalne argumenty na wysokim szczeblu. Ale znowu zwykle nie dzieje się nic, co byłoby bliskie jednoznacznej, rygorystycznej definicji poprawności lub dowodu poprawności.

W matematyce ludzie koncentrują się na poprawności. W rozwoju oprogramowania jest wiele rzeczy, o które programiści muszą się troszczyć, i są między nimi kompromisy. Posiadanie oprogramowania wolnego od błędów lub nawet dobrej definicji poprawności (przy zmieniających się wymaganiach w czasie) to ideał, ale należy się nim zająć w stosunku do innych czynników, a jednym z najważniejszych jest czas poświęcony na rozwijanie go poprzez istniejące programiści. Tak więc w praktyce w lepszych miejscach cel i procesy zmniejszają ryzyko błędów tak bardzo, jak jest to wykonalne, a nie sprawiają, że oprogramowanie jest wolne od błędów.

Jest już wiele dobrych odpowiedzi, ale jest jeszcze więcej powodów, dla których matematyka i programowanie nie są takie same.

1 Dowody matematyczne są zwykle znacznie prostsze niż programy komputerowe. Rozważ pierwsze kroki hipotetycznego dowodu:

Niech będzie liczbą całkowitą

Niech b będzie liczbą całkowitą

Niech c = a + b

Jak dotąd dowód jest w porządku. Przekształćmy to w pierwsze kroki podobnego programu:

Niech a = input ();

Niech b = input ();

Niech c = a + b;

Mamy już mnóstwo problemów. Zakładając, że użytkownik naprawdę wprowadził liczbę całkowitą, musimy sprawdzić granice. Czy jest większy niż -32768 (lub cokolwiek to jest min int w twoim systemie)? Czy mniej niż 32767? Teraz musimy sprawdzić to samo dla b . I dlatego dodaliśmy i b program nie jest poprawna, chyba A + Bjest większy niż -32768 i mniejszy niż 32767. To 5 oddzielnych warunków, które programista musi martwić się, że matematyk może zignorować. Programiści nie tylko muszą się o nie martwić, ale muszą dowiedzieć się, co zrobić, gdy jeden z tych warunków nie jest spełniony, i napisać kod, który zrobi, gdy tylko zdecyduje, jak sobie z nimi poradzić. Matematyka jest prosta. Programowanie jest trudne.

2 Pytający nie mówi, czy odnosi się do błędów w czasie kompilacji, czy w czasie wykonywania, ale ogólnie programiści po prostu nie dbają o błędy w czasie kompilacji. Kompilator je znajdzie i można je łatwo naprawić. Są jak literówki. Jak często ludzie wpisują kilka akapitów bez błędów za pierwszym razem?

3 Szkolenie.Od najmłodszych lat uczymy się matematyki i ciągle spotykamy się z konsekwencjami drobnych błędów. Wyszkolony matematyk musiał zacząć rozwiązywać wieloetapowe problemy z algebrą zwykle w gimnazjum i musiał robić dziesiątki (lub więcej) takich problemów co tydzień przez rok. Pojedynczy upuszczony znak ujemny spowodował, że cały problem był zły. Po algebrze problemy stały się dłuższe i trudniejsze. Z drugiej strony programiści zwykle mają znacznie mniej formalne szkolenie. Wielu jest samoukami (przynajmniej na początku) i nie ukończyło formalnego szkolenia aż do uniwersytetu. Nawet na poziomie uniwersyteckim programiści muszą wziąć udział w kilku zajęciach z matematyki, podczas gdy matematycy prawdopodobnie wzięli jedną lub dwie klasy programowania.

Podoba mi się odpowiedź Yuvala, ale chciałem się z niej trochę pozbyć. Jednym z powodów, dla których łatwiej jest pisać dowody matematyczne, może być sprowadzenie się do tego, jak platoniczna jest ontologia matematyki. Aby zobaczyć, co mam na myśli, rozważ następujące kwestie:

• Funkcje matematyczne są czyste (cały wynik wywołania funkcji jest całkowicie zamknięty w wartości zwracanej, która jest deterministyczna i obliczana całkowicie na podstawie wartości wejściowej).
• Matematyka nie ma mutacji ani zmiany przypisania (gdy trzeba modelować takie rzeczy, używane są funkcje i sekwencje).
• Matematyka jest referencyjnie przejrzysta (np. Nie ma wskaźników, nie ma pojęcia nazwa-nazwa vs nazwa-wartość), a obiekty matematyczne mają semantykę równości ekstensywnej (jeśli „dwie” rzeczy są takie same pod każdym możliwym do zaobserwowania sposobem, to tak naprawdę są to samo).

Chociaż jest dyskusyjne, czy powyższe ograniczenia ułatwiają pisanie programu, myślę, że istnieje ogólna zgoda, że ​​powyższe ograniczenia ułatwiają rozumowanie programu. Najważniejszą rzeczą, którą robisz, pisząc dowód matematyczny, jest powód, dla którego piszesz obecnie (ponieważ w przeciwieństwie do programowania, nigdy nie musisz powielać wysiłku w matematyce, ponieważ abstrakcje są bezpłatne), więc na ogół warto nalegać na powyżej ograniczeń.

Podstawowe dowody matematyczne nie stanowią aplikacji w świecie rzeczywistym, zaprojektowanej w celu zaspokojenia potrzeb żywych ludzi.

Ludzie zmienią swoje pragnienia, potrzeby i wymagania w codziennych programach komputerowych.

Co takiego różni się w pisaniu bezbłędnych dowodów matematycznych i pisaniu bezbłędnego kodu komputerowego, który sprawia, że ​​ten pierwszy jest o wiele łatwiejszy do opanowania niż drugi?

Przy tak wyraźnym wymaganiu jak problem matematyczny można napisać bezbłędny program. Udowodnienie, że algorytm Dijkstry może znaleźć najkrótszą ścieżkę między dwoma punktami na wykresie, nie jest tym samym, co implementacja programu, który akceptuje dowolne dane wejściowe i znajduje najkrótsze punkty między dowolnymi dwoma punktami na wykresie.

Należy zarządzać pamięcią, wydajnością i sprzętem. Chciałbym, abyśmy nie myśleli o tych, pisząc algorytmy, że moglibyśmy do tego wykorzystać czyste i funkcjonalne konstrukcje, ale programy komputerowe żyją w „prawdziwym” świecie sprzętu, podczas gdy dowód matematyczny tkwi w… „teorii”.

Lub, aby być bardziej zwięzłym :

Patrząc na to z innej perspektywy, w środowisku nieakademickim często sprowadza się to do pieniędzy.

Jak twierdzą inne posty, matematyka jest pojedynczą abstrakcyjną specyfikacją, dlatego dowód musi działać konsekwentnie w obrębie tej specyfikacji, aby został udowodniony. Program komputerowy może działać na wielu implementacjach abstrakcyjnej specyfikacji matematycznej - to znaczy, w jaki sposób jeden język lub producent sprzętu implementuje matematykę zmiennoprzecinkową może nieznacznie różnić się od innego, co może powodować niewielkie wahania wyników.

Jako takie, „sprawdzenie” programu komputerowego przed jego napisaniem wiązałoby się z udowodnieniem logiki na poziomie sprzętowym, na poziomie systemu operacyjnego, na poziomie sterownika, języka programowania, kompilatora, może interpretera i tak dalej, dla każdej możliwej kombinacji sprzętu, którą program można uruchomić i wszelkie możliwe dane, które może on pobierać. Ten poziom przygotowania i zrozumienia prawdopodobnie znajdziesz w misjach kosmicznych, systemach broni lub systemach kontroli energii jądrowej, gdzie awaria oznacza dziesiątki miliardów utraconych dolarów i potencjalnie wiele ofiar śmiertelnych, ale niewiele więcej.

Dla Twojego „codziennego” programisty i / lub firmy znacznie bardziej opłacalne jest zaakceptowanie pewnego poziomu dokładności w większości poprawnego kodu i sprzedaż użytecznego produktu, a programiści mogą usunąć błędy, odkrywając je podczas jego działania. stosowanie.

Myślę, że twoje rozumowanie jest prawidłowe, ale twój wkład nie jest. Dowody matematyczne po prostu nie są bardziej odporne na błędy niż programy, jeśli oba są napisane przez ludzi. Cytowano już Dijkstrę, ale zaoferuję dodatkową wycenę.

Musimy jednak zorganizować obliczenia w taki sposób, aby nasze ograniczone moce były wystarczające, aby zagwarantować, że obliczenia osiągną pożądany efekt. Ta organizacja obejmuje skład programu i tam mamy do czynienia z kolejnym problemem dotyczącym wielkości, mianowicie. długość tekstu programu i powinniśmy dać temu problemowi również wyraźne uznanie. Powinniśmy być świadomi faktu, że zakres, w jakim możemy czytać lub pisać tekst, zależy w dużej mierze od jego rozmiaru. [...]

W tym samym nastroju chciałbym zwrócić uwagę czytelnika na fakt, że „klarowność” ma wyraźne aspekty ilościowe, o czym wielu matematyków, co ciekawe, wydaje się być nieświadomych. Twierdzenie stwierdzające ważność wniosku, gdy spełnione są dziesięć stron pełnych warunków, nie jest wygodnym narzędziem, ponieważ wszystkie warunki należy weryfikować za każdym razem, gdy odwołuje się to twierdzenie. W geometrii euklidesowej twierdzenie Pitagorasa dotyczy dowolnych trzech punktów A, B i C, tak że przez A i C można narysować linię prostopadłą do linii prostej przez B i C. Ilu matematyków docenia, że ​​twierdzenie to ma zastosowanie, gdy niektóre czy wszystkie punkty A, B i C pokrywają się? wydaje się to jednak w dużej mierze odpowiedzialne za wygodę, z jaką można zastosować twierdzenie Pitagorasa.

Podsumowując: jako powolna istota ludzka mam bardzo małą głowę i powinienem nauczyć się z nią żyć, szanować moje ograniczenia i w pełni je doceniać, zamiast próbować je ignorować, ponieważ ten drugi próżny wysiłek będzie ukarany niepowodzeniem.

Zostały lekko zredagowane trzy ostatnie akapity z pierwszego rozdziału Programowania strukturalnego Dijkstry.

Aby sformułować to inaczej, lepiej zastosować się do pytania: poprawność jest w dużej mierze funkcją wielkości twojego dowodu. Prawidłowość długich dowodów matematycznych jest bardzo trudna do ustalenia (wiele opublikowanych „dowodów” żyje w otchłani niepewności, ponieważ nikt ich nie weryfikował). Ale jeśli porównasz poprawność trywialnych programów do trywialnych dowodów, prawdopodobnie nie będzie zauważalnej różnicy. Jednak zautomatyzowani asystenci proof (w szerszym znaczeniu tego słowa, twój kompilator Java jest także asystentem proof), pozwalają programom wygrywać, automatyzując wiele prac przygotowawczych.

Jak inne odpowiedzi dotknęły ich odpowiedzi (chcę to rozwinąć), ale dużą część problemu stanowi użycie biblioteki. Nawet przy doskonałej dokumentacji (tak powszechnej jak kod bezbłędny) niemożliwe jest przekazanie pełnej wiedzy o bibliotece każdemu programiście korzystającemu z biblioteki. Jeśli programiści nie rozumieją doskonale swojej biblioteki, mogą popełniać błędy podczas jej używania. Czasami mogą powodować krytyczne błędy, które są wykrywane, gdy kod nie działa. Ale w przypadku drobnych błędów mogą one pozostać niezauważone.

Podobna sytuacja byłaby, gdyby matematyk wykorzystał istniejące dowody i lematy bez ich pełnego zrozumienia; ich własne dowody byłyby prawdopodobnie błędne. Chociaż może to sugerować rozwiązanie, to idealna nauka każdej używanej biblioteki; jest to praktycznie bardzo czasochłonne i może wymagać wiedzy w dziedzinie, której programista nie posiada (niewiele wiem o sekwencjonowaniu DNA / syntezie białek, ale mogę pracować z tymi koncepcjami przy użyciu bibliotek).

Mówiąc bardziej zwięźle, inżynieria oprogramowania (ogólnie inżynieria) opiera się na kapsułkowaniu różnych poziomów abstrakcji, aby umożliwić ludziom skupienie się na mniejszych obszarach problemu, w którym się specjalizują. Pozwala to na rozwijanie wiedzy specjalistycznej w swojej dziedzinie, ale wymaga również doskonałej komunikacji między każdą warstwą. Gdy ta komunikacja nie jest doskonała, powoduje problemy.

Spróbuję być oryginalny po tych wszystkich wspaniałych odpowiedziach.

Programy są dowodami

Curry-Howard izomorfizm mówi nam, rodzaje w programie są twierdzenia i rzeczywisty kod jest ich dowodem.

Trzeba przyznać, że jest to bardzo abstrakcyjny i wysoki poziom poglądu. Problem, który prawdopodobnie masz na myśli, polega na tym, że pisanie typowego kodu jest trudniejsze, ponieważ staje się zbyt niskie. W większości przypadków „musisz powiedzieć maszynie, co ma robić”. Albo spojrzeć na to z innej strony: matematycy są naprawdę dobrzy w abstrakcji.

Na marginesie: „Muzyka strumieni” jest jednym z najpiękniejszych pomostów między nimi. Zasadniczo konfiguruje rzeczy, aby móc powiedzieć „Chcę tego w ten sposób”, a maszyna magicznie robi to dokładnie tak, jak sobie tego życzy.

Żadna z wielu innych odpowiedzi nie wskazuje na następujące. Dowody matematyczne działają na wyimaginowanych systemach obliczeniowych, które mają nieskończoną pamięć i nieskończoną moc obliczeniową. Mogą zatem przechowywać dowolnie duże liczby z nieskończoną precyzją i nie tracą precyzji w żadnych obliczeniach.

$\pi$

To nie jest. Dowody matematyczne są z natury równie błędne, po prostu ich czytelnicy są bardziej tolerancyjni niż kompilator. Podobnie czytelnicy programu komputerowego łatwo dają się zwieść przekonaniu, że jest poprawny, przynajmniej dopóki nie spróbują go uruchomić.

Na przykład, jeśli spróbujemy przetłumaczyć dowód matematyczny na język formalny, taki jak ZFC, będzie on również zawierał błędy. To dlatego, że te dowody mogą być naprawdę długie, więc jesteśmy zmuszeni napisać program do wygenerowania dowodu. Niewiele osób zadaje sobie trud, na własne ryzyko, chociaż prowadzone są aktywne badania nad sformalizowaniem podstawowych dowodów.

I rzeczywiście, matematyka może uzyskać BSOD! To nie byłby pierwszy raz!

Ta ortodoksyjna idea, że ​​wszystkie matematyczne dowody, które zostały dostatecznie zweryfikowane, są zasadniczo poprawne lub mogą być poprawione, jest tym samym, co motywuje twój projekt oprogramowania w pracy: tak długo, jak pozostaniemy na mapie drogowej, usuniemy wszystkie błędy i funkcje kompletne - jest to iteracyjny proces prowadzący do określonego produktu końcowego.

Oto druga strona. Słuchaj, mamy już środki, zweryfikowaliśmy koncepcję biznesową, wszystkie dokumenty są tutaj, abyś je przeczytał. Potrzebujemy tylko ciebie do wykonania i to pewne!

Nie żałujmy też Hilberta , wiedział, w co się pakuje. To tylko biznes.

Jeśli chcesz być naprawdę pewien, weź wszystko indywidualnie i wyciągnij własne wnioski!

Widzę dwa ważne powody, dla których programy są bardziej podatne na błędy niż dowody matematyczne:

1: Programy zawierają zmienne lub obiekty dynamiczne zmieniające się w czasie, podczas gdy obiekty matematyczne w dowodach są zwykle statyczne. Tak więc notacja matematyczna może być wykorzystana jako bezpośrednie wsparcie rozumowania (a jeśli a = b, pozostaje tak w przypadku), gdy nie działa to w programach. Ponadto problem ten staje się znacznie poważniejszy, gdy programy są równoległe lub mają wiele wątków.

2: Matematyka często zakłada stosunkowo dokładnie zdefiniowane obiekty (wykresy, rozmaitości, pierścienie, grupy itp.), Podczas gdy programowanie dotyczy bardzo niechlujnych i raczej nieregularnych obiektów: arytmetyka o skończonej precyzji, skończone stosy, konwersje liczb całkowitych, wskaźniki, śmieci, które wymagają zbierania itp. Dlatego bardzo trudno jest pamiętać o zbiorze warunków związanych z poprawnością.

Powinieneś rozróżnić dwie różne „kategorie”:

• pseudo-proofs (lub pseudo-kod) - to właśnie widzisz w książkach. Jest napisany w języku naturalnym (np. W języku angielskim). Właśnie tego powinieneś nauczyć się matematyki (lub algorytmów).
• formalne dowody (lub kod formalny) - piszesz je, gdy potrzebujesz dowodu (lub kodu), aby być mechanicznie weryfikowalnym (lub wykonywalnym). Taka reprezentacja nie wymaga żadnej „ludzkiej inteligencji”. Można to zweryfikować (lub wykonać) mechanicznie, wykonując niektóre predefiniowane kroki (zwykle dzisiaj wykonywane przez komputery).

Używamy pseudokodu od tysięcy lat (np. Algorytm Euclids). Pisanie formalnego kodu (w językach formalnych, takich jak C lub Java) stało się niezwykle popularne i przydatne po wynalezieniu komputerów. Niestety, formalne dowody (w językach formalnych, takich jak Principia Mathematica lub Metamath) nie są zbyt popularne. A ponieważ każdy pisze dziś pseudo-proofy, ludzie często kłócą się o nowe proofy. Błędy w nich można znaleźć lata, dekady, a nawet wieki po faktycznym „udowodnieniu”.

Nie mogę znaleźć referencji, ale myślę, że Tony Hoare powiedział kiedyś coś w następujący sposób: Różnica między sprawdzaniem programu a sprawdzaniem dowodu polega na tym, że dowód można sprawdzić dwie linie na raz.

Jednym słowem: miejscowość.

Dowody są napisane, aby można je było łatwo sprawdzić. Programy są pisane, aby można je było wykonać. Z tego powodu programiści zwykle pomijają informacje, które byłyby przydatne dla osoby sprawdzającej program.

Rozważ ten program, w którym x jest tylko do odczytu

    assume x >= 0
    p := 0 ;
    var pp := 0 ;
    while( x >= pp + 2*p + 1 ) 
    {
        var q := 1 ;
        var qq := q ;
        var pq := p ;
        while(  pp + 4*pq + 4*qq <= x )
        {
            q, pq, qq := 2*q, 2*pq, 4*qq ;
        }
        p, pp := p + q, pp + 2*pq + qq ;
    }
    assert  p*p <= x < (p+1)*(p+1)

Jest łatwy do wykonania, ale trudny do sprawdzenia.

Ale jeśli dodam z powrotem brakujące twierdzenia, możesz sprawdzić program lokalnie, po prostu sprawdzając, czy każda sekwencja przypisań jest poprawna, uwzględniając jej warunki wstępne i końcowe oraz że dla każdej pętli warunek końcowy pętli jest implikowany przez niezmienny i negacja osłony pętli.

    assume x >= 0
    p := 0 ;
    var pp := 0 ; 
    while( x >= pp + 2*p + 1 ) 
        invariant p*p <= x 
        invariant pp == p*p
        decreases x-p*p 
    {
        var q := 1 ;
        var qq := q ; 
        var pq := p ; 
        while(  pp + 4*pq + 4*qq <= x )
            invariant (p+q)*(p+q) <= x
            invariant q > 0 
            invariant qq == q*q 
            invariant pq == p*q 
            decreases x-(p+q)*(p+q)
        {
            q, pq, qq := 2*q, 2*pq, 4*qq ;
        }
        assert (p+q)*(p+q) <= x and pp==p*p and pq==p*q and qq==q*q and q>0
        p, pp := p + q, pp + 2*pq + qq ;
    }
    assert  p*p <= x < (p+1)*(p+1)

Wracając do pierwotnego pytania: dlaczego zapisywanie dowodów matematycznych jest bardziej odporne na błędy niż pisanie kodu komputerowego? Ponieważ proofy zostały zaprojektowane w taki sposób, aby mogły być łatwo sprawdzone przez ich czytelników, są one łatwo sprawdzane przez ich autorów, a zatem autorzy alarmów zwykle nie popełniają (lub przynajmniej zachowują) logicznych błędów w swoich proofach. Podczas programowania często nie zapisujemy przyczyny, dla której nasz kod jest poprawny; w wyniku tego zarówno czytelnikom, jak i autorowi programu trudno jest sprawdzić kod; w rezultacie autorzy popełniają (a następnie przechowują) błędy.

Ale jest nadzieja. Jeśli pisząc program, również zanotujemy powód, dla którego uważamy, że program jest poprawny, wówczas możemy sprawdzić kod podczas pisania i tym samym napisać mniej błędów. Ma to również tę zaletę, że inni mogą czytać nasz kod i sami go sprawdzać.

Moglibyśmy zapytać, czy w praktyce trudniej jest , lub w zasadzie , pisać proofy lub pisać kod.

W praktyce sprawdzanie jest znacznie trudniejsze niż kodowanie. Bardzo niewiele osób, które wzięły dwa lata matematyki na studiach, może pisać dowody, nawet te trywialne. Wśród osób, które wzięły dwa lata CS na poziomie uczelni, prawdopodobnie co najmniej 30% może rozwiązać FizzBuzz .

Ale w zasadzie istnieją fundamentalne powody, dla których jest odwrotnie. Dowody można, przynajmniej w zasadzie, sprawdzić pod kątem poprawności za pomocą procesu, który nie wymaga żadnej oceny ani zrozumienia. Programy nie mogą - nie możemy nawet stwierdzić, za pomocą żadnego przepisanego procesu, czy program się zatrzyma.

Tylko niewielką część prawdziwych stwierdzeń matematycznych można praktycznie udowodnić. Co ważniejsze, niemożliwe byłoby zbudowanie nietrywialnego (*) zestawu aksjomatów matematycznych, który pozwoliłby na sprawdzenie wszystkich prawdziwych stwierdzeń. Gdyby tylko trzeba było pisać programy wykonujące niewielki ułamek tego, co można zrobić za pomocą komputerów, możliwe byłoby pisanie oprogramowania o możliwej do udowodnienia poprawności, ale często wzywa się komputery do robienia rzeczy wykraczających poza zakres tego, co można udowodnić oprogramowanie może osiągnąć.

(*) Możliwe jest zdefiniowanie zestawu aksjomatów, które pozwoliłyby na wyliczenie wszystkich prawdziwych stwierdzeń, a tym samym ich udowodnienie, ale generalnie nie są one bardzo interesujące. Chociaż możliwe jest formalne zaklasyfikowanie zbiorów aksjomatów do tych, które są względnie nietrywialne, względnie rzecz biorąc, kluczową kwestią jest to, że możliwe do udowodnienia istnienie zdań, które są prawdziwe, ale których nie można udowodnić, nie jest wadą w zestawie aksjomatów. Dodanie aksjomatów, aby uczynić wszystkie istniejące stwierdzenia prawdziwymi, ale niemożliwymi do udowodnienia, sprawiłyby, że inne stwierdzenia stałyby się prawdziwe, ale bez nich można by je udowodnić.

1. Programy komputerowe są testowane w prawdziwym świecie. Podstępny błąd techniczny w długim dowodzie matematycznym, który może zrozumieć tylko ograniczona liczba osób, ma duże szanse na pozostanie niezauważonym. Ten sam rodzaj błędu w oprogramowaniu może powodować dziwne zachowanie, które zauważą zwykli użytkownicy. Więc przesłanka może być niepoprawna.

2. Programy komputerowe wykonują użyteczne funkcje w świecie rzeczywistym. Aby to zrobić, nie muszą być w 100% poprawne, a wysokie standardy poprawności są dość drogie. Dowody są przydatne tylko wtedy, gdy faktycznie coś udowodnią, więc pominięcie części „w 100% poprawnej” nie jest opcją dla matematyków.

3. Dowody matematyczne są jasno określone. Jeśli dowód jest wadliwy, autor popełnił błąd. Występuje wiele błędów w programach komputerowych, ponieważ wymagania nie zostały poprawnie zakomunikowane lub występuje problem z kompatybilnością z czymś, o czym programista nigdy nie słyszał.

4. Nie można udowodnić, że wiele programów komputerowych jest poprawnych. Mogą rozwiązywać nieformalnie zdefiniowane problemy, takie jak rozpoznawanie twarzy. Lub mogą być jak oprogramowanie do prognozowania na giełdzie i mają formalnie określony cel, ale obejmują zbyt wiele zmiennych z prawdziwego świata.

Dużą część matematyki jako działalności człowieka stanowi rozwój języków specyficznych dla danej dziedziny, w których weryfikacja dowodów jest łatwa dla człowieka.

Jakość dowodu jest odwrotnie proporcjonalna do jego długości i złożoności. Długość i złożoność często zmniejsza się, opracowując dobrą notację opisującą sytuację, o której piszemy, wraz z koncepcjami pomocniczymi oddziałującymi w ramach danego rozważanego dowodu.

Nie jest to łatwy proces, a większość dowodów poświadczonych przez osoby usunięte z czołówki badań zdarza się w dziedzinach matematycznych (takich jak algebra i analiza), które miały setki, jeśli nie tysiące lat, podczas których notacja tego pola miała został dopracowany do tego stopnia, że ​​faktyczne spisanie dowodów wydaje się dziecinnie proste.

Jednak w czołówce badań, szczególnie jeśli pracujesz nad problemami, które nie są w obszarach o ugruntowanej lub dobrze rozwiniętej notacji, postawiłbym trudność nawet napisania poprawnego dowodu zbliżającego się do trudności napisania właściwego programu. Wynika to z faktu, że musielibyście jednocześnie napisać analog projektu języka programowania, wytrenować sieć neuronową w zakresie prawidłowej kompilacji, spróbować napisać w tym dowód, zabraknąć pamięci, spróbować zoptymalizować język, iteruj mózg, ucząc się języka, napisz dowód ponownie itp.

Powtarzam, myślę, że pisanie poprawnych dowodów może podchodzić do trudności w pisaniu poprawnych programów w niektórych obszarach matematyki, ale te obszary są z konieczności młode i słabo rozwinięte, ponieważ samo pojęcie postępu w matematyce jest ściśle powiązane z łatwym dowodem weryfikacja.

Innym sposobem na sformułowanie tego, co chcę powiedzieć, jest to, że zarówno języki programowania, jak i matematyka są na końcu zaprojektowane, aby programy komputerowe i dowody były możliwe do skompilowania. Po prostu kompilacja programu komputerowego odbywa się na komputerze i zapewnia poprawność składniową, która zwykle nie ma wiele wspólnego z poprawnością samego programu, podczas gdy „kompilacja” dowodu jest wykonywana przez człowieka i zapewnia poprawność składniową, która jest taka sama jak poprawność dowodu.

Szczerze porównujesz tutaj jabłka i pomarańcze. Fault-dowód i wolna od błędów nie to samo.

Jeśli program porównuje liczby 2i 3tak mówi 2 is greater than 3, może to wynikać z błędnej implementacji:

# Buggy implementation
function is_a_greater_than_b(a,b):
  return b > a

Program jest jednak nadal bezbłędny. Porównując dwie liczby ai b, zawsze będzie mógł powiedzieć, czy bjest większy niż a. To nie jest to, o co ty (programista) miałeś poprosić komputer.

a) Ponieważ programy komputerowe są ważniejsze od dowodów matematycznych

a.1) Uważam, że przy pisaniu złożonego programu komputerowego jest więcej ludzi niż podczas pisania dowodu matematycznego. Oznacza to, że margines błędu jest wyższy.

b) Ponieważ prezesi / akcjonariusze bardziej troszczą się o pieniądze niż naprawianie drobnych błędów , tymczasem Ty (jako programista) musisz wykonywać swoje zadania, aby spełnić niektóre wymagania / terminy / dema

c) Ponieważ możesz być programistą bez „głębokiej” wiedzy z zakresu comp sci, tymczasem byłoby to trudne w matematyce (wierzę)

Do tego:

NASA:

To oprogramowanie jest wolne od błędów. Jest doskonały, tak doskonały, jak to osiągnęli ludzie. Rozważ te statystyki: w trzech ostatnich wersjach programu - każda o długości 420 000 linii - wystąpił tylko jeden błąd. Ostatnie 11 wersji tego oprogramowania zawierało 17 błędów.

Podejmij aktualizację oprogramowania, aby umożliwić wahadłowiecowi nawigację z satelitami Global Positioning Satellites, zmiana obejmująca zaledwie 1,5% programu lub 6 366 linii kodu. Specyfikacje tej zmiany obejmują 2500 stron, o objętości większej niż książka telefoniczna. Specyfikacje dla bieżącego programu zajmują 30 woluminów i obejmują 40 000 stron.

https://www.fastcompany.com/28121/they-write-right-stuff

Poziomy podstawowe:

W przypadku matematyki mamy:
2 + 3 = 5

Dowiedziałem się o tym, gdy byłem bardzo, bardzo młody. Potrafię spojrzeć na najbardziej podstawowe elementy: dwa obiekty i trzy obiekty. Wspaniały.

Do programowania komputerów większość ludzi używa języka wysokiego poziomu. Niektóre języki wysokiego poziomu można nawet „skompilować” w jednym z niższych języków wysokiego poziomu, np. C. C można następnie przetłumaczyć na język asemblera. Język asemblera jest następnie konwertowany na kod maszynowy. Wiele osób uważa, że ​​złożoność się na tym kończy, ale tak nie jest: nowoczesne procesory traktują kod maszynowy jako instrukcje, ale następnie uruchamiają „mikro kod”, aby faktycznie wykonać te instrukcje.

Oznacza to, że na najbardziej podstawowym poziomie (w przypadku najprostszych struktur) mamy teraz do czynienia z mikrokodem, który jest wbudowany w sprzęt i którego większość programistów nawet nie używa bezpośrednio, ani nie aktualizuje. W rzeczywistości nie tylko większość programistów nie dotyka mikrokodu (0 poziomów wyższych niż mikro kod), większość programistów nie dotyka kodu maszynowego (1 poziom wyżej niż mikro kod), ani nawet zestawu (2 poziomy wyższe niż mikro kod) ( z wyjątkiem być może nieco formalnego szkolenia podczas studiów). Większość programistów spędza czas tylko o 3 lub więcej poziomów wyżej.

Ponadto, jeśli spojrzymy na Zgromadzenie (które jest tak niskie, jak zwykle ludzie), każdy pojedynczy krok jest zazwyczaj zrozumiały dla osób przeszkolonych i posiadających zasoby do interpretacji tego kroku. W tym sensie asemblacja jest znacznie prostsza niż język wyższego poziomu. Jednak montaż jest tak prosty, że wykonywanie skomplikowanych zadań, a nawet miernych zadań, jest bardzo żmudne. Języki wyższego poziomu uwalniają nas od tego.

W prawie dotyczącym „inżynierii wstecznej” sędzia oświadczył, że nawet jeśli teoretycznie kod może być obsługiwany jeden bajt na raz, współczesne programy zawierają miliony bajtów, więc dla tego rodzaju rekordów (takich jak kopie kodu) należy utworzyć wysiłek, aby być wykonalnym. (Dlatego rozwój wewnętrzny nie został uznany za naruszenie ogólnej zasady prawa autorskiego „nie robienie kopii”). (Prawdopodobnie myślę o tworzeniu nieautoryzowanych kartridży Sega Genesis, ale mogę myśleć o czymś powiedzonym w sprawie Game Genie. )

Modernizacja:

Czy korzystasz z kodu przeznaczonego na 286s? A może uruchamiasz 64-bitowy kod?

Matematyka wykorzystuje podstawy, które sięgają tysiącleci. W przypadku komputerów ludzie zwykle uważają inwestowanie w coś sprzed dwudziestu lat za bezużyteczne marnowanie zasobów. Oznacza to, że matematyka może być o wiele dokładniej przetestowana.

Standardy używanych narzędzi:

Nauczono mnie (przez znajomego, który odbył bardziej formalne szkolenie z programowania komputerowego niż ja), że nie ma czegoś takiego jak bezbłędny kompilator C, który spełnia specyfikację C. Wynika to z faktu, że język C zasadniczo zakłada możliwość korzystania z nieskończonej pamięci na potrzeby stosu. Oczywiście od takiego niemożliwego wymogu trzeba było odstąpić, gdy ludzie próbowali stworzyć użyteczne kompilatory, które działałyby na rzeczywistych maszynach, które mają nieco bardziej skończony charakter.

W praktyce odkryłem, że dzięki JScript w Windows Script Host udało mi się osiągnąć wiele dobrych zastosowań. (Podoba mi się środowisko, ponieważ zestaw narzędzi potrzebny do wypróbowania nowego kodu jest wbudowany w nowoczesne wersje systemu Microsoft Windows). Korzystając z tego środowiska, zauważyłem, że czasami nie ma łatwo dostępnej dokumentacji dotyczącej działania obiektu. Jednak korzystanie z obiektu jest tak korzystne, że i tak to robię. Więc napisałbym kod, który może być błędny jak gniazdo szerszeni, i robiłbym to w ładnie otoczonym piaskownicą środowisku, w którym widzę efekty i dowiaduję się o zachowaniu obiektu podczas interakcji z nim.

W innych przypadkach, czasami dopiero po ustaleniu, jak zachowuje się obiekt, stwierdziłem, że obiekt (w pakiecie z systemem operacyjnym) jest wadliwy i że jest to znany problem, który Microsoft celowo zdecydował, że nie zostanie naprawiony .

W takich scenariuszach, czy polegam na OpenBSD, stworzonym przez mistrzowskich programistów, którzy regularnie tworzą nowe wydania zgodnie z harmonogramem (dwa razy w roku), ze słynnym zapisem bezpieczeństwa „tylko dwóch odległych dziur” od ponad 10 lat? (Nawet mają łatki erraty dla mniej poważnych problemów.) Nie, w żadnym wypadku. Nie polegam na takim produkcie o tak wyższej jakości, ponieważ pracuję dla firmy, która wspiera firmy dostarczające ludziom komputery korzystające z systemu Microsoft Windows, więc na tym powinien działać mój kod.

Praktyczność / użyteczność wymagają pracy na platformach, które ludzie uważają za użyteczne, i jest to platforma, która jest bardzo niebezpieczna dla bezpieczeństwa (mimo że od samego początku tysiąclecia dokonano ogromnych ulepszeń, które znacznie pogorszyły produkty tej samej firmy) .

Podsumowanie

Istnieje wiele powodów, dla których programowanie komputerowe jest bardziej podatne na błędy i jest to akceptowane przez społeczność użytkowników komputerów. W rzeczywistości większość kodu jest napisana w środowiskach, które nie będą tolerować bezbłędnych wysiłków. (Niektóre wyjątki, takie jak opracowanie protokołów bezpieczeństwa, mogą wymagać nieco więcej wysiłku w tym zakresie.) Oprócz powszechnie myślących powodów, dla których firmy nie chcą inwestować więcej pieniędzy i nie dotrzymują sztucznych terminów, aby zadowolić klientów, istnieje wpływ marsz technologii, który po prostu stwierdza, że ​​jeśli spędzisz zbyt dużo czasu, będziesz pracować na przestarzałej platformie, ponieważ rzeczy zmieniają się znacząco w ciągu dekady.

Od razu pamiętam, jak byłem zaskoczony tym, jak krótkie były niektóre bardzo przydatne i popularne funkcje, kiedy zobaczyłem kod źródłowy strlen i strcpy. Na przykład strlen mógł być czymś w rodzaju „int strlen (char * x) {char y = x; while ( (y ++)); return (yx) -1;}”

Jednak typowe programy komputerowe są znacznie dłuższe. Ponadto wiele współczesnych programów będzie wykorzystywać inny kod, który może być mniej dokładnie przetestowany, a nawet być błędny. Dzisiejsze systemy są znacznie bardziej skomplikowane niż to, co można łatwo przemyśleć, z wyjątkiem ręcznego wymachiwania wielu drobiazgów jako „szczegółów obsługiwanych przez niższe poziomy”.

Ta obowiązkowa złożoność i pewność pracy ze złożonymi, a nawet niewłaściwymi systemami sprawia, że ​​programowanie komputerowe jest dużo sprzętem do weryfikacji niż wiele matematyki, w których sprawy sprowadzają się do znacznie prostszych poziomów.

Kiedy rozkładasz rzeczy w matematyce, dochodzisz do pojedynczych elementów, które dzieci mogą zrozumieć. Większość ludzi ufa matematyce; przynajmniej podstawowa arytmetyka (lub przynajmniej liczenie).

Kiedy naprawdę rozkładasz programowanie komputerowe, aby zobaczyć, co dzieje się pod maską, kończysz się zepsutymi implementacjami złamanych standardów i kodu, który ostatecznie jest wykonywany elektronicznie, a ta fizyczna implementacja jest tylko o jeden krok poniżej mikrokodu, który daje większość wyszkolonych informatyków nie waż się dotykać (nawet jeśli są tego świadomi).

Rozmawiałem z niektórymi programistami, którzy są na studiach lub absolwentami, którzy wprost sprzeciwiają się pomysłowi, że można napisać kod bez błędów. Zrezygnowali z tej możliwości i chociaż przyznają, że niektóre imponujące przykłady (które udało mi się wykazać) są przekonującymi argumentami, uważają takie próbki za niereprezentatywne rzadkie błędy i nadal odrzucają możliwość liczenia na takie wyższe standardy. (Znacznie inne podejście niż o wiele bardziej wiarygodne podstawy, które widzimy w matematyce).

Dowody matematyczne opisują „co” wiedza, a programy opisują „jak” wiedza.

Pisanie programów jest bardziej złożone, ponieważ programiści muszą rozumować o wszystkich różnych stanach, które mogą się pojawić, oraz o zmianach zachowań programu. Dowody używają rozumowania formalnego lub kategorycznego, aby udowodnić pewne rzeczy na temat innych definicji.

Większość błędów jest spowodowana procesami wchodzącymi w stany, których programista nie przewidział. W programie zwykle masz tysiące lub, w dużym systemie, miliony możliwych zmiennych, które nie są danymi statycznymi, ale faktycznie zmieniają sposób działania programu. Wszystkie te oddziałujące razem tworzą zachowania, których nie można przewidzieć, zwłaszcza w nowoczesnym komputerze, na którym zmieniają się warstwy abstrakcji.

Dowód nie zmienia stanu. Definicje i przedmioty dyskusji są ustalone. Udowodnianie wymaga ogólnego myślenia o problemie i rozważania wielu przypadków, ale przypadki te są ustalane przez definicje.