Can math.atan2 return INF?
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
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.