(July 2, 2019 at 12:19 pm)A Toy Windmill Wrote:(July 2, 2019 at 11:36 am)Jehanne Wrote: CS does not have any issues with Cantorian mathematics, such as infinite Turning machines.And intuitionistic mathematics doesn't have issue with Turing machines either. They aren't particularly "Cantorian."
The most notable attraction of intuitionism, however, is in type theory, where type systems display a glaring analogy with logic that is celebrated as the Curry-Howard Correspondence. This has been upgraded to The Holy Trinity with the ever growing popularity of category theory in CS. The analogy is nearly always specifically with an intuitionistic logic, being also a logic that is automatically focused on computable functions, which CS people have a bias towards.
Then "intuitionistic mathematics" is not finitism.