Citace: stud 21. 03. 2016, 14:03:40Citace: Radek Miček 19. 03. 2016, 16:16:38Citace: stud 19. 03. 2016, 15:06:58Máme teď ve škole (VŠ) logiku a nějak zatím nevidím souvislost s IT. Mohl by mi tu někdo dát nějaký příklad, proč by mě měla jako programátora zajímat?Programy lze chápat jako důkazy v určité logice (říká se tomu Curry-Howardův izomorfismus). Důsledkem toho jsou programovací jazyky jako například Coq, kde můžete psát certifikované programy - příkladem takového programu je CompCert. Existuje nějaký podobný příklad praktického uplatnění i pro teorii množin?https://i.stack.imgur.com/KDi5d.png
Citace: Radek Miček 19. 03. 2016, 16:16:38Citace: stud 19. 03. 2016, 15:06:58Máme teď ve škole (VŠ) logiku a nějak zatím nevidím souvislost s IT. Mohl by mi tu někdo dát nějaký příklad, proč by mě měla jako programátora zajímat?Programy lze chápat jako důkazy v určité logice (říká se tomu Curry-Howardův izomorfismus). Důsledkem toho jsou programovací jazyky jako například Coq, kde můžete psát certifikované programy - příkladem takového programu je CompCert. Existuje nějaký podobný příklad praktického uplatnění i pro teorii množin?
Citace: stud 19. 03. 2016, 15:06:58Máme teď ve škole (VŠ) logiku a nějak zatím nevidím souvislost s IT. Mohl by mi tu někdo dát nějaký příklad, proč by mě měla jako programátora zajímat?Programy lze chápat jako důkazy v určité logice (říká se tomu Curry-Howardův izomorfismus). Důsledkem toho jsou programovací jazyky jako například Coq, kde můžete psát certifikované programy - příkladem takového programu je CompCert.
Máme teď ve škole (VŠ) logiku a nějak zatím nevidím souvislost s IT. Mohl by mi tu někdo dát nějaký příklad, proč by mě měla jako programátora zajímat?