Computer Proof vs. Proofs by Hand

This article, rendered as a dialogue between "Quisani" and the author, is presented in the following sections:

(untitled introduction) | Quisani enquires about the relevance of constructivism to computer sceince. | |

1 | Paradoxes and the Related Foundational Crisis | Platonism is introduced and blamed for the antinomies in informal set theory. The significance of these matters for the foundations of mathematics is discussed. |

2 | Constructivism | Constructivism is introduced, its (lack of) impact touched upon. |

3 | Good Things About Constructivism | Five benign effects are attributed to constructivism, falling short of the truth of any part of its critique of classical mathematics. |

4 | Computer Proofs vs. Proofs by Hand | Mainly about proofs of programs arising from constructive existence proofs. Touching upon the "four colour problem" kind of computer proof. |

5 | Critique of Constructivism | Constructivism is criticised, first because of the value of the non-constructive methods which it abjures, and secondly because the concern for effectiveness did not embrace the study of feasibility. |

© created 96/1/15 modified 97/2/3