Iowa Type Theory Commute

Higher-order functions help make it possible to program in a point-free style, where we use combinators to connect functions, rather than calling the functions on inputs explicitly.  

Discussion of datatypes for tree-like data structures in functional languages.  Usefulness of these for processing structured linguistic artifacts, where the structure is represented by the tree structure.

Start of discussion of some of technology and culture that lead to more concise code in functional programming languages.  Type inference to avoid writing types for local and input variables.  Some basics of static and dynamic typing.

Introduction to the basic idea of functional programming.  Three kinds are discussed: functional programming with mutable state, pure functional programming (where there is no implicit state), and strong functional programming (which is pure functional programming where every function is statically required to terminate).

Discussion of some practicalities of applying formal methods to software.  Ideally we are seeking techniques that can be applied with increasing effort to yield increasingly strong results.  Also, introduction to functional programming.

Continuing pessimistic discussion about the purpose of formal methods for Computer Science.  But then counter arguments about the value of absolutely correct software.

Discussion of a technical reason for lack of adoption of computer-checked proofs for mathematics, namely the level of detail in the proof.  Proof assistants require too much detail in proofs to allow mathematicians to carry over their elegant art of expressing just the right amount of information to convey the idea of the proof to a mathematically competent reader.  For Computer Science, a problem...

Some discussion of why computer-checked proofs have not been adopted more in mathematics.  The psychology of telling mathematicians their time-honored method of investigation is inadequate and they need computer-checked proofs.  Computer-checked proofs and certainty.

Some pockets of interest in computer-checked proofs in the US in the 1980s and 1990s.  Several important research projects and initiatives in the US in the late 1990s and early 2000s that helped raise awareness in the US of computer-checked proofs: proof-carrying code, the POPLmark challenge.

Computer-checked proofs can ensure properties of software.  Discussion of several aspects of this idea.

Further discussion of computer-checked proofs, including the example of the proof by Hales and his collaborators of the Kepler Conjecture.  Automath also mentioned.  DAO hack on Ethereum and the interest in cryptocurrency community in computer-checked proofs.

First episode of the Iowa Type Theory Commute.  The basic idea of computer-checked proofs.  The example of the original proof of the Four Color Theorem.