[AnonimoweMirkoWyznania]

#anonimowemirkowyznania
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

[AnonimoweMirkoWyznania]

Zaplusuj ten komentarz, aby otrzymywać powiadomienia o odpowiedziach w tym wątku. Kliknij tutaj, jeśli chcesz skopiować listę obserwujących

[Asterling]

@AnonimoweMirkoWyznania: Załóż sobie konto bo pomimo że zapewne merytoryczne to jednak to nie jest wyznanie więc drugi raz nie dodam.

[FuLame]

@AnonimoweMirkoWyznania: Mam jakies problemy z oczami bo nie widze zadnych materialow dodanych przez ciebie. To gdzie mam szukac tych bledow i niejasnosci?

[cevilo]

@AnonimoweMirkoWyznania: Jest bardzo wiele języków nie będących kompletnymi w sensie Turinga, chociażby SQL. Miałeś pewnie na myśli języki o jakimś zasięgu, bo przecież bardzo wiele języków programowania to jakieś eksperymenty, projekty badawcze, zabawy.

[OhRene]

@AnonimoweMirkoWyznania: Ciekawe! Zakładaj konto i wrzucaj dalsze części.

[elektron_]

Taktyk

[AnonimoweMirkoWyznania]

OP: @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

[FuLame]

@AnonimoweMirkoWyznania: Ach ok, szukalem linku i szukalem "http". Jednak mam problemy z oczami. Dzieki, z checia zajrze.

[c.....a]

@AnonimoweMirkoWyznania: skoro w Coqu napisano kompilator C, a ten jest kompletny w sensie Turinga, to czy sam Coq nie jest kompletny?

[LeD7]

@AnonimoweMirkoWyznania: Możesz podać kilka przykładów wykorzystania tego języka. Dobrze jeżeli przykłady będą zróżnicowane pod względem skomplikowania. Czy można dowieść prawdziwości twierdzenia o czterech barwach przy jego pomocy?

[AnonimoweMirkoWyznania]

OP: @calka_stochastyczna
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

[c.....a]

@AnonimoweMirkoWyznania: jeżeli komuś ciężko nauczyć się matematyki z wykładu, to Coq moim zdaniem w niczym mu nie pomoże, wręcz przeciwnie.