Can math.atan2 return INF?

[Paul Rubin]

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.