Remember the big brouhaha back in the late 19th and early 20th century about the foundations of mathematics? There was one radical school of thought, the Intuitionists, who insisted on constructive proofs. They held the method of "indirect proof", i.e. suppose what you wish to prove is false, and then show that a contradiction results, to be invalid, and disagreed with the "law of the excluded middle", that any given proposition is either true or false.
This was pretty controversial stuff, and David Hilbert wrote the following famous line about it: taking the principle of the excluded middle from the mathematician is the same as denying the telescope to the astronomer, or the boxer the use of his fists.
As a programmer brought up on imperative languages, I have to wonder whether those of similar training feel about pure applicative languages the way Hilbert did about intuitionism.
random notes and thoughts, mostly about Haskell these days, of a rather past middle-aged programmer
Subscribe to:
Post Comments (Atom)
Riddler Classic, May 23, 2020—Holy Mackerel!
Another one using Peter Norvig's word list . It turns out that the word "mackerel" has a curious property: there is exactly ...
-
Back in the Cretaceous era I worked at the University of Oklahoma as a student assistant at Remote 1. OU was a [shudder] IBM big iron shop a...
-
You've probably heard about how the notion of sum types (e.g. Algol 68 union s, Rust enum s, Haskell type s) and product types (e.g. tup...
-
Verbal Abuse as Entertainment When I grew up, my parents always told me that there was a sort of person who needed to tear down others t...
No comments:
Post a Comment