Steven D'Aprano <st...@pearwood.info> writes: > If Intuitionism influenced computer science, where is the evidence of this? > Where are the Intuitionist computer scientists?
Pretty much all of them, I thought. E.g. programs in typed lambda calculus amount to intuitionistic proofs of the propositions given in the types (this is the Curry-Howard correspondence). Languages like Coq and Agda use the correspondence directly so you can state a specification as a type, then prove the type as a theorem, and then extract the proof as executable code which is certified to implement the specification. The trendy area now is called "homotopy type theory", but I don't understand even a tiny bit of it. Intro to Coq: www.cis.upenn.edu/~bcpierce/sf/current/index.html Proofs and types: www.paultaylor.eu/stable/Proofs+Types.html Homotopy type theory: github.com/HoTT , homotopytypetheory.org There's also a wiki at ncatlab.org which is in the intersection of logic and CS, that develops a lot of this stuff. > On the contrary, academic CS seems to have come from the Logicist > school of thought Do you mean formalist? I thought that logicism was the idea that mathematics could be derived from pure logic, and thus it went away when Gӧdel's incompletness theorems appeared. -- https://mail.python.org/mailman/listinfo/python-list
