pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-27 23:06:20 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Note required Coq version

Browse source
This commit is contained in:
Adam Chlipala 2023-02-19 16:23:56 -05:00
parent 2ef93d36fc
commit 04be648f88
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
frap_book.tex
View file

@ -84,7 +84,7 @@ In this early version, you get to take the author's word for it that we are abou
However, one overarching element of our strategy is important enough to deserve to be called out here. However, one overarching element of our strategy is important enough to deserve to be called out here.
We will study a variety of different approaches for formalizing what a program should do and for proving that a program does what it should. We will study a variety of different approaches for formalizing what a program should do and for proving that a program does what it should.
At every step, we will pay close attention to the \emph{common foundation} that underlies everything. At every step, we will pay close attention to the \emph{common foundation} that underlies everything.
For one thing, we will be proving all of our theorems with the Coq proof assistant, a powerful framework for writing and machine-checking proofs. For one thing, we will be proving all of our theorems with the Coq proof assistant\footnote{The author only makes an effort to keep the associated Coq code working with the latest Coq version, which is 8.16 as of this writing.}, a powerful framework for writing and machine-checking proofs.
Coq itself is based on a relatively small set of core features, much like a well-designed programming language, and in both we build up increasingly sophisticated abstractions as libraries. Coq itself is based on a relatively small set of core features, much like a well-designed programming language, and in both we build up increasingly sophisticated abstractions as libraries.
Those features can be thought of as the core of all mathematical reasoning. Those features can be thought of as the core of all mathematical reasoning.