Welcome to Learn Functional Programming: The Computing Foundations of Trustworthy Systems (LFP). LFP is a first course in computer science for students with no prior coursework or experience in computer science or programming. This site supports a social network of researchers, educators, sponsors, and, eventually, students who are supporting, developing, taking, and evaluating this course and its approach. Distinguishing characteristics of this course include:

  • use of a modern constructive logic proof assistant as a programming environment
  • early introduction to inductive definitions, recursion, polymorphism, overloading, abstraction
  • construction of a standard library on the bare logic of the proof assistant using no built-in libraries
  • development of basic expression and imperative languages built on this student-constructed library
  • interwoven topics in computer science (e.g., satisfiability) and software engineering (e.g., modularity)
  • exploration of the realization of these concepts in modern industrial languages (currently Python)
  • preparation for study of logic (assertion languages) in computer science (i.e., formal methods)
  • emphasis on anticipation and avoidance of failure in systems that society will come to rely upon

A related site will host a second course, Learn Proof Engineering: The Logical Foundations of Trustworthy Systems (LPE). For more information on LFP, visit the Course page. Join this site to connect with a private network of interested educators, researchers, and students. This site is evolving, and is still in an early state as of 4/2017. Course content will begin to appear shortly. Comments are welcome and sought.

These courses are responsive to the recent call by Ball and Zorn to teach foundational principles early in the computer science curriculum . The course uses the Lean theorem prover being developed by Leo de Moura at Microsoft Research and the Visual Studio Code programming environment, including Lean and Python plugins. Jeremy Avigad has similarly used Lean to teach an undergraduate course on Logic and Proof at Carnegie Mellon University .

These courses draw in part from Benjamin Pierce’s Software Foundations , and from a much longer line of courses teaching CS1 using other, mostly weakly typed, functional languages, notably Lisp-based languages such as Scheme and Racket. Relevant works include Kiczales’s CS1 course at the University of British Columbia , Findler et al., , back to Abelson and Sussman .

Distinguishing this course from earlier course designs are, among other things, (1) its use of the dependently typed language of a constructive logic proof assistant for CS1, and (2) its “constructive” approach to teaching, where students build everything from the bare logic of the proof assistant on up. Elaborating on (1), it provides students with an exceptionally logically clean and expressive type system, enables a rigorous grounding of the course in type theory, unlike the Lisp-based courses provides static type checking, and crucially, it lines students up for follow-on work on uses of mathematical logic in computer science, formal methods in software and systems engineering, and proof engineering for the verification of critical systems.

Share this
Skip to toolbar