Dlaczego zapisywanie dowodów matematycznych jest bardziej odporne na błędy niż pisanie kodu komputerowego?

190

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ąć.XYX Y X XXXYXX

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.

użytkownik56834
źródło
3
Czy znasz dowody poprawności programów, zarówno na papierze, jak i zmechanizowane w dowodach twierdzeń? Oba istnieją i są sprzeczne z aktualizacją. prawda jest taka, że ​​programowanie, jak się powszechnie naucza, ma niewiele wspólnego z programowaniem z dowodami poprawności.
Blaisorblade,
76
Przypomina mi cytat Knutha, myślę: „Strzeż się powyższego kodu! Udowodniłem tylko, że jest poprawny, nigdy go nie testowałem”
Hagen von Eitzen,
Komentarze nie są przeznaczone do rozszerzonej dyskusji; ta rozmowa została przeniesiona do czatu .
Gilles
7
Znajdź mi ręcznie napisany dowód matematyczny, który ma 100 milionów linii i nie zawiera „błędów”, a dam ci wszystko, co posiadam.
Davor,
Programy funkcjonalne mogą być znacznie łatwiejsze do napisania niż dowody, jednak gdy tylko nadejdzie stan ... trudność eksploduje ...
aoeu256

Odpowiedzi:

226

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.

Yuval Filmus
źródło
Komentarze nie są przeznaczone do rozszerzonej dyskusji; ta rozmowa została przeniesiona do czatu .
DW
1
Czy to możliwe, że w przyszłości asystenci ds. Proofów będą wykorzystywani do sprawdzania zarówno kodu, jak i dowodu? Może czas nauczyć się Agda ? (przepraszam ...)
Alex Vong,
3
@AlexVong Jednym z problemów jest to, że napisanie formalnej specyfikacji dla nietrywialnego kodu (abyś mógł sprawdzić, czy kod faktycznie spełnia specyfikację) jest prawie niemożliwe. Na przykład, czy możesz sobie wyobrazić, jak skomplikowana byłaby formalna specyfikacja przeglądarki (w tym cała interakcja użytkownika, wszystkie obsługiwane formaty plików i protokoły itp.)?
svick,
2
@svick Masz rację, w przypadku interakcji użytkownika czasem nie jest nawet jasne, jakie zachowanie powinno być właściwe. Zamiast tego powinniśmy skupić się na czymś o właściwej specyfikacji formalnej (np. Dowód, kompilator).
Alex Vong,
1
W rzeczy samej. Może to również wyjaśniać, dlaczego wiele osób uważa kodowanie w językach niższego poziomu za znacznie bardziej nużące i mniej zabawne niż kodowanie w językach abstrakcyjnych wysokiego poziomu. Chociaż może to oczywiście różnić się w zależności od osoby (niektórym może się nawet podobać budowanie obwodów sprzętowych / elektronicznych o bardzo niskim poziomie niż pisanie na nich działającego oprogramowania? Ponadto kod niższego poziomu może być w wielu przypadkach niezastąpiony i dobrze pisać sama w sobie może być rzadką umiejętnością / wyceną godną pochwały).
Xji
77

(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

Omar
źródło
3
Chodzi o „ponowne użycie kodu” dość apropos. Tłumaczenie długiego dowodu z rosyjskiego na angielski wymaga sporo pisania ; ale przetłumaczenie dużego programu komputerowego z, powiedzmy, C ++ na Javę, wymaga sporo myślenia . Wskrzeszenie 3000-letniego dowodu w starożytnej Grecji jest równie proste; wskrzeszenie 30-letniego programu w PL / 1 jest tak samo trudne lub trudniejsze.
Quuxplusone
2
Uświadomiłem sobie również przykład starożytnej Grecji: programiści używają tonu lokalnego slangu i potocznych, takich jak (void*)1i open('/dev/null'), które mogą nawet nie być przenośne między różnymi subkulturami, nie mówiąc już o tłumaczeniu na język docelowy. (Czytelnik po prostu musi pogłębić swoją przybliżoną semantykę dzięki długiemu doświadczeniu.) Myślę, że matematyczne dowody zawierają mniej tego rodzaju „slangu”. Jeśli dowód używa słowa, jego rzeczywiste uniwersalne znaczenie powinno być jakoś wydedukowane przez czytelnika. Programy komputerowe nie mają nawet uniwersalnego znaczenia!
Quuxplusone
1
+1, ponieważ jako konstruktywista szalejące domniemanie odrębne od arbitralnie dużej wartości doprowadza mnie do szału. Zmienia się to z błędu na poziomie wartości do logicznego błędu, gdy matematycy zaczynają mówić o nieskończonej serii, a następnie argumentują na podstawie tych serii, powodując błąd na równi z ukrytym - 0 błąd. 00
Nat
@Nat możesz rozwinąć? Nie rozumiem
Gregory Magarshak
@GregoryMagarshak Ta odpowiedź pokazuje przypadek, w którym założenie, że nieskończoność jest ważna w konstrukcji szeregowej, prowadzi do błędu, który opisałem jako taki ukryty- błąd00(„ukryta” wersja niższa w sekcji Wikipedia). Klasyczny matematyk mógłby powiedzieć, że błąd polegał na założeniu, że szereg nieskończony jest zbieżny, chociaż konstruktywista określiłby błąd jako nieuzasadnione domniemanie nieskończoności.
Nat
55

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.

Dyskretna jaszczurka
źródło
2
Jestem tylko laikiem; o czym tak naprawdę mówił Dijkstra przez „programowanie”?
Ovi
2
@Ovi Nie jestem do końca pewien, ale główna różnica polega na tym, że mówi on o (nietrywialnych) algorytmicznych rozwiązywaniu problemów bardziej niż o „ogólnych” zadaniach programistycznych, tzn. Z pewnością nie mówi o jakimś programie CRUD, który musi połączyć istniejące architektury lub inne komponenty itp. Więcej na temat opinii Dijkstry na temat programowania można znaleźć w tej odpowiedzi
Dyskretna jaszczurka
3
Głosuj za cytowanie Dijkstry, ale wybrałeś niewłaściwe miejsce! Wiele napisał o tym problemie w pierwszych akapitach programowania strukturalnego. Nie chciałbym zmieniać twojej odpowiedzi, przesyłając inną ofertę, ale mam nadzieję, że zechcesz dodać więcej z tego artykułu do swojej odpowiedzi!
wvxvw
@Ovi zgaduję, że programowanie w czasach Dijkstry częściej oznaczało pisanie kodu asemblującego w porównaniu z nowoczesną erą języków wysokiego poziomu. Podobnie czytam wydanie Mythical Man-Month z 1974 roku, koncepcje są wciąż aktualne, ale referencje techniczne to asembler na poziomie systemu lub PL / I, znacznie różniący się od tego, co większość ludzi myśli o programowaniu dzisiaj
JimLohse
46

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.

Aleksiej Romanow
źródło
6
Ten sam artykuł: „Dowody anegdotyczne sugerują, że aż jedna trzecia wszystkich artykułów opublikowanych w czasopismach matematycznych zawiera błędy - nie tylko drobne błędy, ale nieprawidłowe twierdzenia i dowody”. To było w latach 90., ale czy dziś jest inaczej? Prawdopodobnie te dokumenty istniejące w tamtych czasach wciąż istnieją i wszystko się układa ... Więc nie jestem całkowicie przekonany, że matematyczne dowody przedstawione w papierach zawierają mniej błędów.
MarkokraM,
Fascynująca anegdota, ale nie widzę, że bezpośrednio odpowiada na pytanie lub nie angażuje się w niego. Czy chcesz edytować swoją odpowiedź, aby bardziej bezpośrednio odpowiadać na zadane pytanie? Czy argumentujesz, że dowody matematyczne są tak samo błędne jak pisanie kodu komputerowego? Czy masz na to dodatkowe dowody? Anegdota lub dwie tak naprawdę tego nie pokazują, prawda?
DW
@DW Wysyłam wiadomość e-mail do Leslie, jeśli może podać dalsze dowody dotyczące roszczenia.
MarkokraM,
3
@DW Leslie powiedział w swojej szczerej odpowiedzi, że jego kolega przeprowadził dochodzenie z 51 dowodami opublikowanymi w tym czasie w Math Reviews. Jego zdaniem jest to więcej niż anegdota, ale nie nadaje się do mocnych dowodów ze względu na kilka faktów. Sprawa była bardziej skomplikowana, ponieważ wystąpiły pewne błędy w dowodach, ponieważ używano błędnych dowodów w celu promowania wcześniej opublikowanych artykułów itp. Byłby to świetny temat badawczy, ale wymaga tyle pracy. W jaki sposób programowo weryfikować dowody matematyczne jest wciąż wielkim pytaniem. Aplikacje stworzone do interaktywnej pomocy próbnej są na bardzo wczesnym etapie. Przynajmniej ich interfejs.
MarkokraM
@DW Anegdota lub dwie pokazują, jak to zrobić sposób dowód matematyczny może wydawać się „poprawny”, ale w rzeczywistości być niesłuszny. Każdemu, kto napisał złożony algorytm komputerowy i wykonał matematyczny dowód, i próbował napisać algorytm komputerowy podobny do matematycznego dowodu, a następnie odkrył, w jaki sposób „algorytm” wysokiego poziomu jest zdradzany przez wiele, wiele błędów w szczegółach, wynik wcale nie jest zaskakujące.
Jak
39

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.

Dan Bryant
źródło
14
+1 za ostatni akapit. Podczas gdy matematyczne dowody są w zasadzie budowane jeden na drugim, zwykle podstawy są dobrze zrozumiałe, analog bibliotek komputerowych (chociaż mają też błędy ...), a faktyczny dowód nie jest zbyt długi. Z kolei oprogramowanie konsumenckie jest długie i skomplikowane, a zatem ma wiele innych możliwości niepowodzenia.
Yuval Filmus,
6
W praktyce drugim problemem związanym z oprogramowaniem konsumenckim jest to, że „prawidłowe” zachowanie jest często źle zdefiniowane z góry, a zatem to, co kiedyś było poprawne, staje się błędne. To tak, jakby próbować napisać dowód, aby dowiedzieć się, że ludzie postanowili zmienić aksjomaty. Możesz to naprawić w notacji, prawda?
Dan Bryant
2
@DanBryant Taka sytuacja zdarza się w matematyce. W szczególności definicje terminów zmieniają się w czasie i często są niejednoznaczne, nawet jeśli są stosowane. Imre Lakatos w „Dowodach i obaleniach” opisuje to terminem „wielokąt”. Podobnie stało się z „funkcją” i, w mniejszym stopniu, „całką”. Nawet dzisiaj „kategoria” nie jest jednoznaczna, a dowody i twierdzenia mogą zawieść w zależności od tego, co dokładnie masz na myśli.
Derek Elkins,
25

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:

x2)+4x+3)x+3)=(x+1)(x+3))x+3)=x+1

x2)+4x+3)x+3)x=-3)

Mehrdad
źródło
3
Świetna odpowiedź! poza tym, że jako komputer sprzeciwiam się użyciu słowa „niepotrzebnie”. ;) [Załóżmy, że był to tylko jeden krok w większym dowodzie mającym na celu udowodnienie, że -xjest złożony. Fakt, że ten krok jest błędny, gdy -x = 3jest bardzo istotny dla poprawności wypełnionego dowodu!]
Quuxplusone
@Quuxplusone: = P
Mehrdad
Komputery mogą również używać symbolicznej matematyki i niedeterministycznych reguł przepisywania, po prostu języki, których używamy, takie jak C ++, są bardzo bardzo niskie i oparte na starożytnej technologii (na przykład C miał mniej funkcji niż Algol 60). Jedynymi wyjątkami są języki sprawdzania / sprawdzania, takie jak Idris / Agda, Lisp z symbolicznymi rozwiązaniami i Mathematica. ja.wolframalpha.com/input/…
aoeu256
23

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

nn!

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.

Ariel
źródło
18

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).
Jeutnarg
źródło
Warto wspomnieć, że ekwiwalent programowy „nieprzemijalności” to czystość funkcjonalna , która jest rozpoznawana i obsługiwana w niektórych językach, takich jak Haskell.
Pharap,
12

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.

Kaveh
źródło
Właściwie nie jestem pewien, kto jest w gorszej sytuacji między programistami a matematykami w formalnym (tj. W sposób sprawdzany maszynowo) formułowaniu specyfikacji poprawności i sprawdzaniu poprawności kodu, powiedzmy, programu 10KLOC lub większego. Z jednej strony masz całkowitą rację, że większość programistów nie ma dobrze rozwiniętych umiejętności dowodzenia twierdzeń. Z drugiej strony, duże formalne proofy są jak duże programy i do zarządzania wymagają zasadniczo umiejętności inżynierii oprogramowania. Jestem całkowicie pewien, że każdy nieformalny dowód poprawności takiego programu nie miałby nadziei na rację.
Derek Elkins,
Może. W każdym razie i tylko dla wyjaśnienia, nie biorę pod uwagę formalnych dowodów w mojej odpowiedzi, tylko nieformalne dowody na poziomie, jaki widzimy w dokumentach z algorytmami.
Kaveh
11

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.

Czytanie
źródło
10

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ń.

Smażony Brice
źródło
7

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 :

wprowadź opis zdjęcia tutaj

Félix Gagnon-Grenier
źródło
4

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.

nawigator_
źródło
3
Wydaje się, że masz wąski pogląd na to, czym jest matematyka i zdecydowanie zbyt ekspansywny pogląd na to, co pociąga za sobą program komputerowy. Nie musisz udowadniać poprawności całego systemu, aby udowodnić poprawność programu, wystarczy udowodnić, że jest poprawny, zakładając, że pozostałe komponenty spełniają ich specyfikacje. Jeśli nie, to nie wina twojego programu. Z drugiej strony, jeśli twój program się zepsuje, ponieważ zależy to od szczegółów, które nie są częścią specyfikacji tych komponentów, np. Wariantów implementacji IEEE754, to twoja wina.
Derek Elkins,
Uczciwy komentarz. Prawdopodobnie niewłaściwie używam terminologii, ponieważ nie jest to moje wykształcenie. Chociaż uważam, że zakładanie, że inne komponenty są bezbłędne, nie jest mądrym posunięciem, z uwagi na moje wcześniejsze komentarze.
navigator_
4

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.

wvxvw
źródło
Co rozumiesz przez „długie dowody matematyczne”? Dowód twierdzenia o mniejszym wykresie jest dość długi, ale tak naprawdę nikt go nie kwestionuje. Twierdzenie Feit-Thompson ma dość długi dowód, ale tak naprawdę nigdy nie było w zawieszeniu. Jak porównujesz długości prób i programów? Liczba słów? Czy naprawdę nie ma zauważalnych różnic między proofami a programami, gdy porównujesz proofy i programy o podobnej złożoności (długości)?
Yuval Filmus
@YuvalFilmus tak jak w cytacie: dziesięć stron stwierdzeń jest długich dla ludzi. Jak oceniać długość programu? Cóż, Dikstra zaproponował metrykę: długość tekstu. Myślę, że może to być zbyt uproszczone, ale mimo to jest dobrą heurystyką. Istnieją inne, bardziej interesujące wskaźniki, takie jak na przykład złożoność cykliczna
wvxvw
3

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.

użytkownik2138038
źródło
3
Zaraz, co sprawia, że ​​myślisz, że matematycy „w pełni rozumieją” dowody i lematy, których używają? Nie jestem pewien, jaką różnicę między matematykami a programistami próbujesz tutaj wykazać.
Derek Elkins,
3

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

Programy 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.

Oleg Łobaczow
źródło
Nie do końca rozumiem, czy to rozwiązuje pytanie. OP nie wskazał, że rozmawiają o językach programowania z potężnymi systemami typów, i myślę, że mają na myśli bardziej ogólne systemy typów. Curry-Howard jest w tym przypadku trochę banalny.
6005
Wiem, że jest to trochę zbyt daleko idące w przypadku C lub podobnych rzeczy. Ale mam na myśli: matematyka jest bliższa niż może się wydawać typowemu początkującemu CS!
Oleg Lobachev
1
Wygląda na to, że jesteś „nieostrożnym obserwatorem” izomorfizmu Curry-Howardsa, o którym wspomniałem w mojej odpowiedzi. Nawet jeśli mamy izomorfizm między programami a dowodami, nie oznacza to, że pisanie programów i pisanie dowodów jest w ogóle podobne. W rzeczywistości może nawet być tak, że wszystkie „interesujące” lub „typowe” programy nie odpowiadają typowemu dowodowi i odwrotnie.
Dyskretna jaszczurka
@Discretelizard Nie jest oczywiste, że „interesujące” programy nie odpowiadają „typowemu dowodowi”. Oto przykład, w którym biorę czyjś „typowy dowód” i tworzę (szkic) niezaprzeczalnie interesujący program (coś ściśle związanego z eliminacją Gaussa). Sądzę, że wyposażone w odpowiednio precyzyjne typy najbardziej interesujące programy byłyby przydatnymi lematami lub twierdzeniami, ale wiele (konstruktywnych) dowodów nie ma rzeczywistego znaczenia obliczeniowego - po prostu weryfikują warunki poboczne - choć bardzo wiele.
Derek Elkins,
3

Ż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.

π

Crobar
źródło
2
„Dowody matematyczne działają na wyimaginowanych systemach obliczeniowych, które mają nieskończoną pamięć i nieskończoną moc obliczeniową”. Większość dowodów matematycznych „działa” na formalnych systemach algebraicznych, np. Na liczbach rzeczywistych (gdzie mamy „nieskończoną precyzję”). Można to również zrobić w programach: istnieją tak zwane systemy algebry komputerowej (CAS), które właśnie to robią! Ponadto całe pola matematyki dotyczą tego, że nie możemy przedstawić wszystkich liczb rzeczywistych dokładnie jako skończonych liczb zmiennoprzecinkowych. Myślę, że rozróżniasz matematykę od programowania tam, gdzie ich nie ma.
Dyskretna jaszczurka
1
@Discretelizard, tak, istnieją specjalne pakiety z dowolną precyzją, ale nawet wtedy dostępna pamięć ograniczy rzeczywistą osiągalną precyzję. Są to również specjalne pakiety. Tylko niewielka część programowania odbywa się za pomocą takich pakietów, głównie w środowisku akademickim.
crobar
π
@Discretelizard, myślę, że mój punkt widzenia nadal jest słuszny, większość programistów nie używa takich systemów CAS. Są o wiele za wolne do programowania w świecie rzeczywistym. Większość programowania zasadniczo obejmuje operacje na liczbach o ograniczonej dokładności. Najpopularniejszymi językami są C, C ++, Python, Java itp. Żaden domyślnie nie używa reprezentacji stylu CAS (chociaż można w nich tworzyć pakiety). Twój kontrprzykład to niewielki niszowy podzbiór języków / systemów komputerowych.
crobar
2
@crobar Problem z twoją odpowiedzią polega na tym, że ogromna większość wykrytych błędów nie jest spowodowana błędami zmiennoprzecinkowymi lub przepełnieniami liczb całkowitych (chociaż te przyczyniają się do przyzwoitej liczby, a te aspekty zdecydowanie sprawiają, że pełna poprawność programu jest znacznie bardziej nieprawdopodobna). Można jednak wysunąć bardziej ogólne twierdzenie, że matematykom brakuje wielu obaw programistów, takich jak wydajność, czas wprowadzenia produktu na rynek, łatwość konserwacji i ograniczona zdolność do zmiany wymagań, jeśli okażą się zbyt trudne.
Derek Elkins,
3

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!

wprowadź opis zdjęcia tutaj

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!

Dan Brumleve
źródło
3

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ą.

René Ahn
źródło
3

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”.

Ivan Kuckir
źródło
3

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ć.

Theodore Norvell
źródło
2

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.

Ben Crowell
źródło
3
Dwa lata po studiach na poziomie matematyki nie znaczy dwa lata koncentrowała się na piśmie dowody (lub wydając żadnego czasu na pisanie dowodów). Powiedział, że mam wrażenie, że to jest wspólne dla średnio- / wczesnych klas szkół średnich geometrycznych zawierać dowody, więc widocznie to można spodziewać się nawet 13-latków, aby móc pisać proste dowody z niespełna roku szkolnego kształcenia dla temat. Obliczenia algebraiczne krok po kroku są również zasadniczo dowodami. Myślę, że stawiasz poprzeczkę za „trywialną”, jeśli chodzi o programowanie o wiele za nisko i za zbyt wysokie.
Derek Elkins,
3
Możemy pisać programy w ten sam sposób. Można sobie wyobrazić wymóg, że każda pisana funkcja / procedura musi zawierać formalną specyfikację i dowód (powiedzmy w Coq), że spełnia specyfikację. Istnieją zatem sposoby na sprawdzenie tego dowodu poprawności w sposób, który nie wymaga żadnej oceny ani zrozumienia.
DW
@DW: Zakładasz, że (1) pożądane zachowanie może być w pełni określone we wszystkich przypadkach, (2) istnieje konieczny dowód (tj. Problem nie jest nierozstrzygalny), oraz (3) jeśli dowód istnieje, wówczas mogę to znaleźć. Myślę, że wszystkie trzy z tych założeń są fałszywe przynajmniej w niektórych przypadkach (prawdopodobnie prawie we wszystkich przypadkach). Re 3, zauważ, że chociaż niektóre dowody mogą być łatwe, wiele dowodów jest bardzo trudnych do znalezienia.
Ben Crowell,
@DerekElkins: Moje twierdzenie, że bardzo niewielu studentów potrafi pisać nawet trywialne dowody, opiera się na moich własnych doświadczeniach z moimi studentami. To jest na uczelni, więc YMMV. Fakt, że niektóre lekcje geometrii w liceum zawierają dużą dawkę korekt, nie przekłada się na fakt, że wszyscy studenci mogą pisać dowody. Powinni także wiedzieć, jak wykonać podstawową algebrę, ale w mojej szkole mniej więcej połowa studentów pierwszego roku nie potrafi - co pomaga wyjaśnić, dlaczego tak wielu zawodzi.
Ben Crowell,
Byłoby to dobre wyjaśnienie, aby dodać do odpowiedzi, aby wyjaśnić, dlaczego nie możesz zastosować tego samego podejścia do sprawdzenia poprawności programu. Ogólnie (2) i (3) rzadko są problemem, ani w praktyce, ani w zasadzie (jeśli nie można udowodnić właściwy program, pisać w inny sposób, dopóki nie można udowodnić, że poprawne). Jednak twoje (1) jest ważną kwestią i myślę, że wzmocniłoby to odpowiedź, wyjaśniając, dlaczego utrudnia to robienie tego samego w przypadku programów, co w przypadku dowodów.
DW
2

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ć.

supercat
źródło
1
„Tylko niewielką część prawdziwych stwierdzeń matematycznych można praktycznie udowodnić”. - Jak mierzysz „porcję”? Czy ma to jakiś rozkład prawdopodobieństwa? Czy masz dowody na poparcie tego oświadczenia?
DW
„komputery są często wzywane do robienia rzeczy wykraczających poza zakres tego, co może udowodnić poprawne oprogramowanie”. - Czy masz na to jakieś dowody? Czy masz przykład? Czy twierdzisz, że „poza tym, co w zasadzie można udowodnić, że jest poprawne” lub „poza tym, co możemy sobie wyobrazić w praktyce”?
DW
@DW: Jeśli X i Y są wyrażeniami ortogonalnymi, które są prawdziwe, ale nie są możliwe do udowodnienia, to dla każdego stwierdzenia P, które można udowodnić, będą co najmniej dwa zdania ortogonalne (P i X) oraz (P i Y), które są prawdziwe, ale nie -dopuszczalny. W przypadku zestawów nieskończonych taka logika niekoniecznie niczego dowodzi, ponieważ można użyć podobnej logiki, aby pokazać, że liczba parzystych liczb całkowitych jest dwa razy większa niż liczba nieparzysta, ponieważ dla każdej nieparzystej liczby całkowitej można zidentyfikować dwie parzyste liczby całkowite (4x) i (4x + 2), które nie są powiązane z żadnymi innymi nieparzystymi liczbami całkowitymi, ale oczywiście parzyste i nieparzyste liczby całkowite mają równą liczność.
supercat
@DW: Wyrażenie „mała część” może zatem naprawdę mieć sens tylko w opisie części prawdziwych stwierdzeń, które można praktycznie udowodnić, ale myślę, że warto zrozumieć, że niemożność udowodnienia wszystkich prawdziwych stwierdzeń nie jest „wadą”. Jeśli chodzi o komputery, wiele pól rutynowo stosuje algorytmy o ekstremalnie małym, ale niezerowym prawdopodobieństwie awarii, a następnie dostosowuje je tak, aby prawdopodobieństwo było akceptowalnie niskie (np. Poniżej prawdopodobieństwa uderzenia sprzętu przez meteoryt). W wielu przypadkach różne tryby awarii nie są jednak niezależne, więc może to być w zasadzie niemożliwe ...
supercat 12.12.2017
... w celu ustalenia prawdopodobieństwa różnych kombinacji awarii. Jeśli oszacuje się prawdopodobieństwo awarii podczas arbitralnego jednominutowego okresu na jeden na 10 ^ -500, można by go wykończyć o setki rzędów wielkości i nadal mieć niezawodny system, ale jeśli ktoś jest wyłączony o 494 rzędy wielkości system ulegałby awarii raz na kilka lat.
supercat
2
  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.

James Hollis
źródło
2

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.

Vladimir Sotirov
źródło
1

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.

Arnab Datta
źródło
2
Jaka jest zatem twoja definicja „usterki” w programie?
user56834,
0

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

Exeus
źródło
„Programy komputerowe są ważniejsze od dowodów matematycznych” To zależy od programu i dowodu. I wiele z tego wydaje się być bardzo spekulacyjnych.
David Richerby
@DavidRicherby cóż, miałem na myśli takie rzeczy, jak twierdzenie Last fermat i Apollo NASA github.com/chrislgarry/Apollo-11 math.wisc.edu/~boston/869.pdf - i nawet nie mówimy o systemach operacyjnych i tak dalej.
Exeus
0

Poziomy podstawowe:

Spójrzmy na rzeczy na najprostszym i najbardziej podstawowym poziomie.

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).

TOOGAM
źródło
1
Podczas gdy robisz niezły argument za złożonością programowania, prawie wcale nie rozważasz matematyki! W rzeczywistości wydajesz się nie doceniać złożoności związanej z matematyką formalną: „Kiedy rozkładasz rzeczy w matematyce, dochodzisz do pojedynczych elementów, które dzieci mogą zrozumieć”, naprawdę ? Poza tym to samo można powiedzieć o wystarczająco „wysokim poziomie” programowania (np. Scratch jest przeznaczony dla dzieci). Zauważ też, że chociaż pełnej specyfikacji C nie można zaimplementować, kompilator obsługujący ważny podzbiór został formalnie poprawny przy użyciu proofów wspomaganych komputerowo.
Dyskretna jaszczurka
Zgoda. W dowodzie na poziomie badań dokładnie nie zobaczysz czegoś na poziomie2)+3)=5. Zamiast tego znajdziesz stwierdzenia typu „można łatwo udowodnić za pomocą X”, gdzie X zajęło ci dwa lata na opanowanie; lub „jest prostym zastosowaniem twierdzenia Y”, w którym Y zajęło dziesiątki lat i dziesiątki osób do udowodnienia. Oczywiście można „skompilować” każdy artykuł badawczy w elementarną, formalną matematykę / logikę - znajdowanie niezliczonych błędów, jestem pewien - ale nikt nie zadaje sobie z tym trudu . (A nie wszyscy zgadzają się, że to jest dobre i dobrze tak niewiele osób. Nie starają się sformalizować matematykę.)
Raphael
Uwaga meta: jeśli jesteś ekspertem w jednej rzeczy i ekspertem początkującym (lub niższym) w innej, jesteś w najgorszej możliwej sytuacji, aby porównać te dwie rzeczy .
Raphael
Dyskretna jaszczurka - to Computer Science SE. Co więcej, po przeczytaniu innych odpowiedzi przed opublikowaniem, poczułem, że dotykają matematyki znacznie bardziej niż komputerów. Czułem, że moja odpowiedź była lepsza, ponieważ nie dodawałem już słów, które byłyby zbędne w stosunku do tego, co napisano gdzie indziej. /// Jeśli chodzi o Scratch, wysoki poziom jest bardziej złożony, a nie prostszy (patrząc na perspektywę pełnego zrozumienia wszystkich ruchomych części). Z tej perspektywy, z której pisałem, montaż jest prostszy niż Scratch na innych warstwach (z jeszcze prostszymi bramkami elektronicznymi NAND)
TOOGAM,
0

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.

Justin Meiners
źródło
2
Powiedziałbym, że matematyczne dowody są w pełni zdolne do opisania wiedzy „co”: weźmy np. Każdy dowód, który konstruuje przykład potwierdzający istnienie lub metodę obliczania wartości. Mimo to zgadzam się, że stan jest czymś nieobecnym w dowodach, w tym sensie, że nie ma innego stanu niż ten wyraźnie opisany przez autora (lub czytelnika!). To właśnie ten stan pozwala programowi zrobić coś, o czym czytelnik / autor nie jest świadomy, podczas gdy jest to niemożliwe w dowodzie. (Oczywiście, dowody mogą mieć niezamierzone cechy lub wyniki, ale wciąż jest potrzebna aktywna myśl, aby je zdobyć)
Dyskretna jaszczurka
@Discretelizard To jest pomocny komentarz. Myślę, że granica między „co” a „jak” jest z pewnością rozmyta. Udowodnienie, że algorytm działa tak, jak myślisz, w rzeczywistości nie opisuje w moim odczuciu „jak”, tylko gwarantuje pewne właściwości. Z filozoficznego punktu widzenia uważam, że wiedza „jak” wymaga korespondencji ze światem. Programy zawsze robią to, co im mówisz. Kiedy masz błąd, to co mu powiedziałeś, nie odpowiada światowi (co modelujesz). Matematyka, niezależna od aplikacji (jak problemy fizyki) wydaje się być całkowicie zależna od spójności.
Justin Meiners