[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Steven D'Aprano <steve at 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.

- Prev by Date:
**Can math.atan2 return INF?** - Next by Date:
**Can math.atan2 return INF?** - Previous by thread:
**Can math.atan2 return INF?** - Next by thread:
**Can math.atan2 return INF?** - Index(es):