References:
[QED at large, Ringer et al., 2019]()
Source of Knowledge [Mechanizing Proof. MacKenzie 2001]
cite: https://www.voxco.com/blog/inductive-vs-deductive-reasoning/
Inductive reasoning is a logical thinking process that integrates observations with experiential information to draw a conclusion. You are employing the use of inductive reasoning every time you look at a set of data and then form general conclusions on knowledge from past experiences.
Inductive research is usually used when there is a lack of existing literature on a topic. This is because there is no existing theory that can be tested on the concept. The inductive training approach can be categorized into the following three stages:
e.g. Use history data, observe a pattern, and to predict the future: Given $6, 9, 12, 15, …$, then what is $n$th number?
Weakness:
A drawback of inductive reasoning is that inferences are made from specific situations that may not have significance in the real world.
When employing deductive reasoning in research, you begin with a theory. This theory is then narrowed down into more specific hypotheses that can be tested. These are further narrowed down into observations that allow us to test the hypothesis to confirm whether the data supports or rejects the hypothesis.
The deductive training approach can therefore be categorized into the following four stages:
Weakness:
Relies on initial premises being correct. Deductive reasoning heavily relies on the initial premises being correct. The final argument is invalid if even one premise is found to be incorrect.
e.g. Mathematic equation solving in the class: $5+\sqrt{(x+14)} = x + 7$
(Static) Type System.
Usage Example of type system:
Python -> Dropbox.
Martin-Lof
? Cornell. NuPRL [Robert Constable] – extract verified programs from proof of correctness.
1980s. France. Calculus of Constructions [Gerard Huet and Thierry Coquand]
1990s. Calculus of Inductive Constructions [Coquand and Christine PaulinMohring]
– The begining of formal methods
@1931. Godel. Incompleteness theorem.
==> We have to admit a certain amount of defeat: if the correctness of our program involves such a proposition, we cannot succeed.
@ 1936. Turing. Halting – Undecidable.
@1951, Henry Gordon Rice. Syracuse University.
这一卷介绍三个内容：
This volume weaves together three conceptual threads:
事实发现，逻辑学对于计算机的作用效果，远远大于在数学领域所起的作用。这个发现起到了标志性的作用，因为近100年来所有的关于逻辑的研究都是来自数学领域。
在计算机领域，归纳证明几乎无处不在。你肯定在以前的离散数学或者算法分析的课程上见到过归纳证明，但是在这个课程中，我们将更为深入的探讨这个方法。
“As a matter of fact, logic has turned out to be siginicantly more effective in computer science than it has been in mathematics. This is quite remarkable, especially since much of the impetus for the development of logic during the past one hundred years came from mathematics.”
“In particular, the fundamental tools of inductive proof are ubiquitous in all of computer science. You have surely seen them before, perhaps in a course on discrete math or analysis of algorithms, but in this course we will examine them more deeply than you have probably done so far.”
逻辑学与计算机科学是互补的学科：计算机学科对逻辑学也是有贡献的。其中一个贡献便是用计算机开发出的用于构造证明的软件工具。这些软件工具包括两大类。
两大类证明器：
Two broad categories of proof assistants:
本教程基于Coq。
Coq的开发开始于1983年，并在近几年获得了学术界和产业界诸多用户的关注。 Coq为机器检查的形式化推理提供了一个丰富的交互式环境。
Coq的核心（kernel）是一个简单的证明检查器（Proof-checker），这个检查器能够保证，只有当推理（deduction）步骤完全正确，才能通过检查。
在核心之外，Coq提供了多种高级手段来辅助证明的构造，包括：
Kernel of Coq:
a simple proof-checker, guarantees that only correct deduction steps are ever performed.
Facilities in Coq:
Coq 在计算机科学和数学领域中的应用有很多方面：
Usages of Coq:
As a platform for modeling programming languages. Examples:
As an environment for developing formally certified software and hardware. Examples:
As a realistic environment for functional programming with dependent types. Examples:
As a proof assistant for higher-order logic. Examples:
Functional programming is:
a family of programming languages designed to emphasize these idioms, including
Its roots go back to Church’s lambda-calculus, invented in 1930s, well before the first electronic computers.
Playing a key role in high-value systems at companies like Jane Street Capital, Microsoft, Facebook, Twitter, and Ericsson.
Most basic tenet: computation should be pure:
For example:
Benefits of pure functional programming
References: Basics: Functional Programming in Coq Functional style of programming is founded on simple, everyday mathematical intuition: If a procedure or method has no side effects, then (ignoring efficiency) all we need to understand about it is how it maps input to outputs. The direct connection between programs and simple mathematical objects supports both formal correctness proofs and sound informal reasoning about program behavior. Features of functional programming in Coq:
If you could revise
the fundmental principles of
computer system design
to improve security...
... what would you change?