Wiki
Clone wikippt / Home
Programs, Proofs and Types: Course wiki
In this course, we study how to write certified programs, i.e. programs together with proofs that they indeed satisfies the requirements of the programs. The proofs are formal, in the sense that their correctness checked by the computer itself. The course uses the proof assistant Coq for this course.
A quick description of Coq and similar systems.
The underlying theory of proof assistants like Coq is a theory of depenent types. One can see such systems as a (functional) programming language with very advanced type. The specifications that the program has to satisfy can be expressed as types in the programming language and proving that a program satisfies a specifications is to write a program of the appropriate type. Thus writing proofs are closely related to programming. Due to the close connections to functional programming, these systems allow ``extracting'' programs which can then be compiled and run.
While our main motivation in this course is the write programs that are formally proved to be correct, systems like coq can be used to formalise and prove mathematical theorems as well.
Getting started.
You need to have a working environment suitable for using Coq. I would recommend installing one of the standard GNU/Linux distributions. Coq comes pre-packaged in most of them. Here are some instructions for getting coq up and running on Debian/Ubuntu
$ sudo apt-get install coq # Install coq $ sudo apt-get install emacs # If you do not have it already $ sudo apt-get install proofgeneral # The proof general mode for emacs
Coq comes with an IDE. While it is okey for basic interaction, any nontrivial development will require you to use an editor with good support for coq. Emacs has very good support for coq via the proof general mode. This is what I recommend for day to day use.
Note: If you have managed to get other editors, vim for example, to work well with coq please include the details here in the wiki.
Proofgeneral problems on Debian/Ubuntu
Unfortunately, it seems that the proof general installed through the
system package manager (of certain Ubuntu and Debian releases) is
often problematic. I have made a minimal init.el, which is
essentially from the proof general website, that configures your emacs
appropriately. It configures emacs
to use the melpa package
repository instead of the system repository. You still need to start
your emacs and install the proof general. See the proof general
website website for more details
mkdir ProofPrograms cd ProofPrograms git clone https://bitbucket.org/piyush-kurur/ppt # Clone this repository mkdir -p ~/.emacs.d # Create the emacs.d directory if it does not exists. cp init.el ~/.emacs.d/ # This will overwrite your emacs config file if there is one # Start emacs and install the packages using # # M-x package-refresh-contents RET # M-x package-install RET proof-general RET
Note M-x means type Alt-x followed by the command given above (you can use tab to complete the command form a prefix).
Updated