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.
[url]http://homepages.inf.ed.ac.uk/wadler/topics/history.html#propositions-as-types[/url]
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:
[url]http://existentialtype.wordpress.com/2011/03/27/the-holy-trinity/[/url]
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.)
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.
http://homepages.inf.ed.ac.uk/wadler/topics/history.html#propositions-as-types
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:
http://existentialtype.wordpress.com/2011/03/27/the-holy-trinity/
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.)
_________________
I don't know half of you half as well as I should like; and I like less than half of you half as well as you deserve.
