#1: Propositions as Types & The Holy Trinity of Computation Autor/ica: Melkor, Lokacija: VoidPostano: 18:35 čet, 13. 3. 2014 — Skrenuo bih pažnju zainteresiranim računarcima (i ostalima) na članak koji IMHO na lijep i osebujan način opisuje duboku vezu između logike i programskih jezika, propozicija i tipova, dokaza i programa.
Logika i programski jezici (preciznije, teorija tipova) dvije su od tri komponente koje čine ono što Bob Harper zove Sveto Trojstvo Izračunavanja (the Holy Trinity of Computation). Treća komponenta je teorija kategorija. Prema Harperovoj doktrini, propozicije, tipovi i strukture, odnosno dokazi, programi i preslikavanja, tri su manifestacije božanskog pojma izračunavanja. Više o tome u nešto starijem tekstu:
Oba autora su vrlo osebujni tipovi s ponešto kontroverznim stavovima, no vrlo su vješti u pisanju, tako da preporučujem i ostale njihove tekstove i članke. (Pogotovo stoga što se, AFAIK, na našem studiju računarstva imate prilike susresti samo s prvom komponentom Trojstva.)
