Irreal

I recently came across an old video of Isaac Asimov being interviewed about his thoughts on science, rationality, and superstition. It’s from 1988 but, sadly, still relevant today. Much of Asimov’s discussion concerns his thoughts about religion but that’s not the part that resonated with me. He also discussed the usual new age nuttiness like astrology—which is hardly new—and all the rest of it. Again, that’s not the part that concerns me.

What did resonate with me was his lamenting the rejection of science on the part of some people. You still see some of that from fringe religious groups like the creationists and others. That’s unfortunate but, again, not what concerns us here.

Rather, it’s the rejection of science for political reasons that should concern us. If you’re thinking, “Yeah, those guys on the other side should knock that off” you’re missing the point. Both sides of the political divide are guilty. Some on the right are all too happy to reject science if interferes with some political belief. A recent example is the inexplicable refusal to wear masks during the pandemic despite clear scientific evidence that they protect not just others but the wearer. Even though it’s a life and death issue, they’d rather hold firm to their political dogma than listen to what science has to say on the matter.

Those on the left aren’t innocent either. They’ll happily suppress scientific findings and punish the scientists responsible for them if they believe they contravene the progressive narrative. They take to Twitter to get the transgressors fired and make them unemployable. It’s not that they don’t believe the science, they simply think that it’s dangerous to permit scientific findings that challenge their received wisdom.

All of these people are dangerous and should be excluded from a polite and rational society. It’s too bad we still have to talk about this after Asimov made such a convincing case for embracing the rational.

Over at Quanta magazine, Kevin Hartnett has an interesting article about using computers in the service of Mathematics. That’s nothing new, of course, but this isn’t about numerical methods or LaTeX, it’s about using computers to help develop mathematical proofs.

Even that notion isn’t new. There is, for instance, Coq, which has been doing the same sort of thing since 1989. What is new is that Mathematicians are trying to capture within another theorem prover, Lean, all known mathematics, or at least all of undergraduate mathematics. That’s a huge undertaking and they’re still only about half done. The hope is that with that knowledge, Lean will know enough to start help proving theorems.

According to the latest Mathlib Statistics, there are currently 19,305 definitions and 41,552 theorems in the system. You can, yourself, play with the system if you like. There are instructions for installing it on all of the usual operating systems or even for running it in a browser, although that will be much slower than a regular installation.

If, like many of us, you come from a Mathematical background, you’ll probably find the article interesting and may want to try the system out.

Most Irreal readers probably know the name Dijkstra, if only from his famous letter to the ACM entitled “Go To Statement Considered Harmful” and his celebrated shortest path algorithm. In fact, Edsger Wybe Dijkstra was a giant in the field of Computer Science, A Turing Award winner, and a significant contributor to both the engineering and theoretical sides of Computer Science.

Krzysztof Apt has a long and interesting biographical article about Dijkstra in Inference. Although he was an astoundingly successful academic, Dijkstra didn’t do much formal publishing. Rather, he preferred to publish much of his work in private reports that he numbered consecutively and prefixed with his initials. There were 1,318 such reports totaling over 7,700 pages. He’d typically send photocopied copies of each report to about 20 colleagues chosen depending on the report’s subject matter.

Dijkstra was interested in formal methods and in particular about writing correct programs. He thought programming should be approached like Mathematics and that every program should come with a formal proof of correctness. He was, according to Apt, a friendly and personable man but his rigidly held views could be off-putting and were often interpreted as arrogance.

Apt’s article has many interesting vignettes from Dijkstra’s life including the fact that when he married he listed his profession as Programmer on the marriage license. The Dutch authorities rejected that on the grounds that there was no such profession. Most surprising of all, perhaps, is that the famous “considered harmful” phrase did not originate with him but was from Niklaus Wirth, an editor of the ACM at the time the letter was published. Dijkstra’s original title was “A Case against the GO TO Statement.”

If you have any interested at all in the history of our field—and, really, you should—you’ll want to read Apt’s article. It full of interesting facts you didn’t know.