Out with a Howl: four public lectures on the occasion of my retirement
- from Boolean Algebra to Unified Algebra, 2012 June 7
This paper was prepared for the 150th anniversary of George Boole's amazing paper that introduced boolean algebra to the world, and published in the Mathematical Intelligencer v.26 n.2 p.3-19, 2004. The mathematical details were published in the International Journal of Mathematical Sciences v.1 n.1 p.20-37, 2007. It was an invited talk at Passau, Alberta, York (UK), Newcastle, Lisbon, and most recently at St.Mary's University, Halifax, 2010.
Boolean algebra is simpler than number algebra, with applications in programming, circuit design, law, specifications, mathematical proof, and reasoning in any domain. So why is number algebra taught in primary school and used routinely by scientists, engineers, economists, and the general public, while boolean algebra is not taught until university, and not routinely used by anyone? A large part of the answer may be in the terminology and symbols used, and in the explanations of boolean algebra found in textbooks. This paper points out some of the problems delaying the acceptance and use of boolean algebra, and suggests some solutions.
- Practical Predicative Programming Primer, 2012 June 8
This talk (or a close relative) was given at a summer school in Turku, at Verified Software: Theories, Tools, and Experiments Toronto, 2008 October 6-9, and at Integrated Formal Methods iFM 2012 June in Pisa.
This talk introduces a method of programming from specifications so that each programming step can be checked by a verifier. Logic errors can be reported the way syntax errors are reported now. Program verification is easier than you think. Invariants and variants are not explicitly needed. The kinds of comments that programmers write, when formalized, are sufficient. And the proofs are well within the abilities of existing provers.
- a Probability Perspective, 2012 June 11
This talk was given at McMaster, UC Irvine, Queen's, Waterloo, and Dalhousie in 2010, and published in Formal Aspects of Computing, v.23 n.4 p.391-419, 2011.
This talk could be called "probability meets programming". It draws together four perspectives that contribute to a new understanding of probability and solving problems involving probability. The first is the Subjective Bayesian perspective that probability is affected by one's knowledge, and that it is updated as one's knowledge changes. The problem of assigning prior probabilities disappears according to the Information Theory perspective, which equates probability with information. The main point of the talk is that the formal perspective (formalize, calculate, unformalize) is beneficial to solving probability problems. And finally, the programmer's perspective provides us with a suitable formalism. To illustrate the benefits of these perspectives, the previously open problem of the two envelopes is completely solved.
- Problems with the Halting Problem, 2012 June 12
This invited talk was presented at COMPUTING 2011 Symposium on 75 years of Turing Machine and Lambda-Calculus, Karlsruhe Germany, 2011 October 20-21. It was presented at the 50th anniversary of IFIP WG2.1 in Rome on 2012 February 7. It has been published in Advances in Computer Science and Engineering v.10 n.1 p.31-60, 2013 March
Either we leave the definition of the halting function incomplete, not saying its result when applied to its own program, or we suffer inconsistency. If we choose incompleteness, we cannot require a halting program to apply to programs that invoke the halting program, and we cannot conclude that it is incomputable. If we choose inconsistency, then it makes no sense to propose a halting program. Either way, the incomputability argument is lost.