Aktywne Wpisy
WielkiNos +435
Ekstrawertyczna juleczka egzaltacyjna dziwi się że pracujący za najniższą krajową kontroler biletów w komunikacji miejskiej nie zna 5 języków i nie skończył co najmniej 2 kierunków studiów.
Zamiast podejść i się po prostu odezwać lepiej nagrać tiktoka pokazującego wszystkim swój skrajny niedobór środka uspokajającego.
#bekaztwitterowychjulek #truestory #logikarozowychpaskow
Zamiast podejść i się po prostu odezwać lepiej nagrać tiktoka pokazującego wszystkim swój skrajny niedobór środka uspokajającego.
#bekaztwitterowychjulek #truestory #logikarozowychpaskow
robert5502 +124
24 listopada 2009 roku John Edward Jones tragicznie stracił życie w jaskini Nutty Putty po wstrząsającej 28-godzinnej męce.
Podczas eksploracji ze swoim bratem Joshem Jones przypadkowo wszedł do zwężonego tunelu, myląc go z innym ciasnym przejściem znanym jako „Kanał Urodzeniowy”.
Utknął do góry nogami w otworze o wymiarach 10 na 18 cali (25 na 46 cm), około 400 stóp (120 m) od wejścia do jaskini.
Jones został uwięziony w pozycji przypominającej hak,
Podczas eksploracji ze swoim bratem Joshem Jones przypadkowo wszedł do zwężonego tunelu, myląc go z innym ciasnym przejściem znanym jako „Kanał Urodzeniowy”.
Utknął do góry nogami w otworze o wymiarach 10 na 18 cali (25 na 46 cm), około 400 stóp (120 m) od wejścia do jaskini.
Jones został uwięziony w pozycji przypominającej hak,
Cześć Mirki. Ostatnio zacząłem na pewnym kole naukowym na pewnej polskiej uczelni prowadzić zajęcia z języka Coq i chciałbym się podzielić z wami tworzonymi przeze mnie materiałami dydaktycznymi: zeimer.github.io
Czym jest Coq? Jest to asystent dowodzenia twierdzeń oraz język programowania oparty na teorii typów. Umożliwia nam programowanie funkcyjne (jak w Haskellu, tylko na sterydach) oraz "robienie matematyki" (definiowanie obiektów matematycznych, dowodzenie ich właściwości etc.). Jest warty uwagi, bo dzięki temu możemy, zamiast pisać testy, po prostu udowodnić, że nasze programy działają poprawnie. Coq jest jedynym znanym mi językiem programowania, który nie jest kompletny w sensie Turinga — jest to konieczne, by nie popaść w sprzeczność (programy, które się zapętlają, w logice odpowiadają sprzeczności). Nie jest to jednak przeszkoda — w Coqu napisano jedyny kompilator języka C, w którym nie ma błędów (udowodniono, że jest poprawny, więc jest poprawny).
Materiały są przeznaczone dla osób umiejących trochę programować (imperatywnie) oraz znających podstawy logiki, ale myślę, że można dać radę i bez tego. Zapraszam do czytania informatyków, którzy chcą się nauczyć nowego sposobu programowania oraz formalnego rozumowania na temat programów (i nie tylko). Zapraszam też matematyków, którzy nie lubią teorii zbiorów i chcieliby dowiedzieć się co nieco o teorii typów, a także o teorii kategorii (planuję napisać o tym w przyszłości).
Obecnie dostępne są 2~ rozdziały: krótki wstęp historyczny oraz rozdział o logice konstruktywnej. Jest też początek rozdziału o typach induktywnych, który piszę na biężąco.
Mam nadzieję, że wam się spodoba. Jeżeli tak — plusujcie, to założe tu konto i będę wam spamował za każdym razem, kiedy dodam coś nowego. Proszę was też o poszukiwanie błędów i niejasności w tekście oraz pisanie swoich sugestii.
#coq #informatyka #matematyka #programowanie #programowaniefunkcyjne #haskell #it
Kliknij tutaj, aby odpowiedzieć w tym wątku anonimowo
Kliknij tutaj, aby wysłać OPowi anonimową wiadomość prywatną
Post dodany za pomocą skryptu AnonimoweMirkoWyznania ( http://mirkowyznania.eu ) Zaakceptował: Asterling
Przepraszam (・へ・)
@FuLame
Podałem link, ale z jakichś powodów nie wyświetla się na niebiesko. Wrzucam jeszcze raz, może tym razem będzie czytelniej: link
@cevilo
Zasadniczo miałem na myśli "poważne" języki (a więc nie personalne eksperymenty), których głównym przeznaczeniem jest programowanie niezawężone do jakiejś specyficznej dziedziny (czyli SQL odpada). Skrót myślowy był konieczny, żeby za dużo nie pisać.
Ten komentarz został dodany przez osobę dodającą wpis
Jedyną dozwoloną w Coqu formą rekursji jest rekursja dobrze ufundowana — wszystkie napisane w Coqu programy kończą pracę. Jeżeli nie jesteś w stanie udowodnić, że program kończy pracę, to nie zostanie zaakceptowany. Skoro nie można napisać programu, który się zapętla, to Coq nie jest kompletny w sensie Turinga. Jak widać, nie przeszkadza to w pisaniu kompilatorów.
@LeD7
Można. Właściwie jest to jeden z najbardziej znanych sukcesów Coqa (poza zweryfikowanym