Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]
Groups > comp.lang.python > #112167
| From | Paul Rubin <no.email@nospam.invalid> |
|---|---|
| Newsgroups | comp.lang.python |
| Subject | Re: Can math.atan2 return INF? |
| Date | 2016-07-31 20:41 -0700 |
| Organization | A noiseless patient Spider |
| Message-ID | <87vazl5f5z.fsf@jester.gateway.pace.com> (permalink) |
| References | (15 earlier) <5774d75d$0$1617$c3e8da3$5496439d@news.astraweb.com> <0765346e-42a1-48b7-8b7d-e134f4165ce4@googlegroups.com> <57755efb$0$1604$c3e8da3$5496439d@news.astraweb.com> <d4e25cbd-38cd-4ca3-afde-4c67692e89ce@googlegroups.com> <579eb9b2$0$1611$c3e8da3$5496439d@news.astraweb.com> |
Steven D'Aprano <steve@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.
Back to comp.lang.python | Previous | Next — Previous in thread | Next in thread | Find similar | Unroll thread
Can math.atan2 return INF? Steven D'Aprano <steve@pearwood.info> - 2016-06-22 03:50 +1000
Re: Can math.atan2 return INF? pdorange@pas-de-pub-merci.mac.com (Pierre-Alain Dorange) - 2016-06-21 20:01 +0200
Re: Can math.atan2 return INF? Jussi Piitulainen <jussi.piitulainen@helsinki.fi> - 2016-06-21 21:32 +0300
Re: Can math.atan2 return INF? Steven D'Aprano <steve@pearwood.info> - 2016-06-22 11:40 +1000
Re: Can math.atan2 return INF? Nagy László Zsolt <gandalf@shopzeus.com> - 2016-06-27 15:27 +0200
Re: Can math.atan2 return INF? Steven D'Aprano <steve@pearwood.info> - 2016-06-22 11:38 +1000
Re: Can math.atan2 return INF? pdorange@pas-de-pub-merci.mac.com (Pierre-Alain Dorange) - 2016-06-22 08:21 +0200
Re: Can math.atan2 return INF? Ben Bacarisse <ben.usenet@bsb.me.uk> - 2016-06-22 16:34 +0100
Re: Can math.atan2 return INF? Random832 <random832@fastmail.com> - 2016-06-22 12:19 -0400
Re: Can math.atan2 return INF? pdorange@pas-de-pub-merci.mac.com (Pierre-Alain Dorange) - 2016-06-22 19:18 +0200
Re: Can math.atan2 return INF? Ben Bacarisse <ben.usenet@bsb.me.uk> - 2016-06-22 20:17 +0100
Re: Can math.atan2 return INF? Lawrence D’Oliveiro <lawrencedo99@gmail.com> - 2016-06-22 12:50 -0700
Re: Can math.atan2 return INF? Steven D'Aprano <steve@pearwood.info> - 2016-06-23 13:59 +1000
Re: Can math.atan2 return INF? Dan Sommers <dan@tombstonezero.net> - 2016-06-23 04:40 +0000
Re: Can math.atan2 return INF? Steven D'Aprano <steve+comp.lang.python@pearwood.info> - 2016-06-23 16:45 +1000
Re: Can math.atan2 return INF? Ben Bacarisse <ben.usenet@bsb.me.uk> - 2016-06-23 15:39 +0100
Re: Can math.atan2 return INF? alister <alister.ware@ntlworld.com> - 2016-06-23 15:04 +0000
Re: Can math.atan2 return INF? Steven D'Aprano <steve@pearwood.info> - 2016-06-24 02:44 +1000
Re: Can math.atan2 return INF? pdorange@pas-de-pub-merci.mac.com (Pierre-Alain Dorange) - 2016-06-23 19:14 +0200
Re: Can math.atan2 return INF? Marko Rauhamaa <marko@pacujo.net> - 2016-06-23 20:22 +0300
Re: Can math.atan2 return INF? pdorange@pas-de-pub-merci.mac.com (Pierre-Alain Dorange) - 2016-06-24 09:53 +0200
Re: Can math.atan2 return INF? Marko Rauhamaa <marko@pacujo.net> - 2016-06-24 13:38 +0300
Re: Can math.atan2 return INF? Gregory Ewing <greg.ewing@canterbury.ac.nz> - 2016-06-26 11:43 +1200
Re: Can math.atan2 return INF? Gregory Ewing <greg.ewing@canterbury.ac.nz> - 2016-06-26 11:40 +1200
Re: Can math.atan2 return INF? Marko Rauhamaa <marko@pacujo.net> - 2016-06-26 10:09 +0300
Re: Can math.atan2 return INF? Gregory Ewing <greg.ewing@canterbury.ac.nz> - 2016-06-27 11:08 +1200
Re: Can math.atan2 return INF? Steven D'Aprano <steve@pearwood.info> - 2016-06-27 12:59 +1000
Re: Can math.atan2 return INF? Marko Rauhamaa <marko@pacujo.net> - 2016-06-27 09:40 +0300
Re: Can math.atan2 return INF? Rustom Mody <rustompmody@gmail.com> - 2016-06-27 06:15 -0700
Re: Can math.atan2 return INF? Marko Rauhamaa <marko@pacujo.net> - 2016-06-27 16:45 +0300
Re: Can math.atan2 return INF? Rustom Mody <rustompmody@gmail.com> - 2016-06-27 07:01 -0700
Re: Can math.atan2 return INF? Marko Rauhamaa <marko@pacujo.net> - 2016-06-27 17:12 +0300
Re: Can math.atan2 return INF? Rustom Mody <rustompmody@gmail.com> - 2016-06-27 07:27 -0700
Re: Can math.atan2 return INF? Marko Rauhamaa <marko@pacujo.net> - 2016-06-27 20:03 +0300
Re: Can math.atan2 return INF? Gregory Ewing <greg.ewing@canterbury.ac.nz> - 2016-06-28 18:12 +1200
Re: Can math.atan2 return INF? Rustom Mody <rustompmody@gmail.com> - 2016-06-27 23:25 -0700
Re: Can math.atan2 return INF? Steven D'Aprano <steve+comp.lang.python@pearwood.info> - 2016-06-28 16:27 +1000
Re: Can math.atan2 return INF? Gregory Ewing <greg.ewing@canterbury.ac.nz> - 2016-06-28 18:12 +1200
Re: Can math.atan2 return INF? Marko Rauhamaa <marko@pacujo.net> - 2016-06-28 09:23 +0300
Re: Can math.atan2 return INF? Random832 <random832@fastmail.com> - 2016-06-28 09:39 -0400
Re: Can math.atan2 return INF? Steven D'Aprano <steve@pearwood.info> - 2016-06-29 01:22 +1000
Re: Can math.atan2 return INF? Marko Rauhamaa <marko@pacujo.net> - 2016-06-28 19:36 +0300
Re: Can math.atan2 return INF? Marko Rauhamaa <marko@pacujo.net> - 2016-06-28 19:42 +0300
Re: Can math.atan2 return INF? Steven D'Aprano <steve+comp.lang.python@pearwood.info> - 2016-06-29 19:35 +1000
Re: Can math.atan2 return INF? Marko Rauhamaa <marko@pacujo.net> - 2016-06-29 13:54 +0300
Re: Can math.atan2 return INF? Lawrence D’Oliveiro <lawrencedo99@gmail.com> - 2016-06-29 18:33 -0700
Re: Can math.atan2 return INF? Rustom Mody <rustompmody@gmail.com> - 2016-06-29 19:13 -0700
Re: Can math.atan2 return INF? Chris Angelico <rosuav@gmail.com> - 2016-06-30 12:38 +1000
Re: Can math.atan2 return INF? Steven D'Aprano <steve+comp.lang.python@pearwood.info> - 2016-06-30 18:24 +1000
Re: Can math.atan2 return INF? Andreas Röhler <andreas.roehler@online.de> - 2016-06-30 11:35 +0200
Re: Can math.atan2 return INF? Lawrence D’Oliveiro <lawrencedo99@gmail.com> - 2016-06-30 02:42 -0700
Re: Can math.atan2 return INF? Andreas Röhler <andreas.roehler@online.de> - 2016-06-30 12:13 +0200
Re: Can math.atan2 return INF? Andreas Röhler <andreas.roehler@online.de> - 2016-06-30 12:11 +0200
Re: Can math.atan2 return INF? Steven D'Aprano <steve@pearwood.info> - 2016-07-01 03:18 +1000
Re: Can math.atan2 return INF? Rustom Mody <rustompmody@gmail.com> - 2016-06-30 08:28 -0700
Re: Can math.atan2 return INF? Steven D'Aprano <steve@pearwood.info> - 2016-07-01 04:03 +1000
Re: Can math.atan2 return INF? Rustom Mody <rustompmody@gmail.com> - 2016-07-01 07:19 -0700
Re: Can math.atan2 return INF? Marko Rauhamaa <marko@pacujo.net> - 2016-07-01 18:20 +0300
Re: Can math.atan2 return INF? Rustom Mody <rustompmody@gmail.com> - 2016-07-29 22:46 -0700
Re: Can math.atan2 return INF? Steven D'Aprano <steve@pearwood.info> - 2016-08-01 12:53 +1000
Re: Can math.atan2 return INF? Paul Rubin <no.email@nospam.invalid> - 2016-07-31 20:41 -0700
Re: Can math.atan2 return INF? Rustom Mody <rustompmody@gmail.com> - 2016-07-31 20:54 -0700
Re: Can math.atan2 return INF? Rustom Mody <rustompmody@gmail.com> - 2016-07-31 21:05 -0700
Re: Can math.atan2 return INF? Ian Kelly <ian.g.kelly@gmail.com> - 2016-08-01 01:05 -0600
Re: Can math.atan2 return INF? Rustom Mody <rustompmody@gmail.com> - 2016-07-24 19:48 -0700
Re: Can math.atan2 return INF? Marko Rauhamaa <marko@pacujo.net> - 2016-06-30 09:24 +0300
Re: Can math.atan2 return INF? Rustom Mody <rustompmody@gmail.com> - 2016-06-29 23:29 -0700
Re: Can math.atan2 return INF? Dennis Lee Bieber <wlfraed@ix.netcom.com> - 2016-06-30 07:47 -0400
Re: Can math.atan2 return INF? alister <alister.ware@ntlworld.com> - 2016-06-30 14:54 +0000
Re: Can math.atan2 return INF? Paul Rubin <no.email@nospam.invalid> - 2016-06-29 23:57 -0700
Re: Can math.atan2 return INF? Lawrence D’Oliveiro <lawrencedo99@gmail.com> - 2016-06-30 00:16 -0700
Re: Can math.atan2 return INF? Paul Rubin <no.email@nospam.invalid> - 2016-06-30 00:32 -0700
Re: Can math.atan2 return INF? Lawrence D’Oliveiro <lawrencedo99@gmail.com> - 2016-06-30 00:39 -0700
Re: Can math.atan2 return INF? Steven D'Aprano <steve+comp.lang.python@pearwood.info> - 2016-06-30 18:27 +1000
Re: Can math.atan2 return INF? Andreas Röhler <andreas.roehler@online.de> - 2016-06-30 09:17 +0200
Re: Can math.atan2 return INF? Lawrence D’Oliveiro <lawrencedo99@gmail.com> - 2016-06-30 00:17 -0700
Re: Can math.atan2 return INF? Gregory Ewing <greg.ewing@canterbury.ac.nz> - 2016-06-30 18:06 +1200
Re: Can math.atan2 return INF? Marko Rauhamaa <marko@pacujo.net> - 2016-06-30 09:32 +0300
Re: Can math.atan2 return INF? Random832 <random832@fastmail.com> - 2016-06-29 09:55 -0400
Re: Can math.atan2 return INF? Gregory Ewing <greg.ewing@canterbury.ac.nz> - 2016-06-26 11:15 +1200
Re: Can math.atan2 return INF? MRAB <python@mrabarnett.plus.com> - 2016-06-26 00:31 +0100
Re: Can math.atan2 return INF? Ben Bacarisse <ben.usenet@bsb.me.uk> - 2016-06-23 20:04 +0100
Re: Can math.atan2 return INF? pdorange@pas-de-pub-merci.mac.com (Pierre-Alain Dorange) - 2016-06-23 19:07 +0200
Re: Can math.atan2 return INF? Ben Bacarisse <ben.usenet@bsb.me.uk> - 2016-06-23 15:37 +0100
csiph-web