FOM: RE: Opinions on place to start considering computation....

[Steve Stevenson]

Ayan Mahalanobis writes:
 > I have always wondered if there is any taker of the idea that computation is
 > essentially a proof by Intuitionistic logic with/without(?) countable
 > choice. That is to say that if I have a proof that there is a fixed point
 > for certain function in Intuitionistic Logic then I can compute it.
 > 
 > This is not a reply to the quoted message but I thought goes along well with
 > the thread.

It had always seemed to me that Errett Bishop's view was a correct
one. Functional languages have reached a point from which we can get
highly efficient code. The thing that was missing constructive set
approach of Bishop...

best
steve