Install Isabelle

Isabelle:
Isabelle is a popular generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical manner.

https://isabelle.in.tum.de/installation.html

Class table

functional programming

Functional programming is a programming paradigm that treats computation as the evaluation of mathematical functions and avoids changing state and mutable data. It emphasizes the application of functions, in contrast to the imperative programming style, which emphasizes changes in state. A simple example of a function in Python, a language that supports both imperative and functional programming, might be:

def add(x, y):
    return x + y

Proof

A proof is a logical argument demonstrating that a certain statement is true. It is based on a set of axioms or previously proven statements. The nature of the proof varies based on the field. For instance, mathematical proofs are based on mathematical logic and are often presented as equations or inequalities.

Interactive Theorem Provers

Interactive theorem provers are tools used to help create formal proofs. Unlike automated provers, they require human guidance. They are typically used in formal verification of software.

Key features include:

• Proof as a Program: A proof here is a script or program that operates on a proof state.

• Proof Tactics and Deduction Rules: These are used to simplify and break down proof goals, making the proof more manageable.

Isabelle/HOL

Isabelle is an interactive theorem prover, and HOL stands for Higher Order Logic, a version of predicate logic that Isabelle implements. It supports a wide range of paradigms including functional programming and has robust support for reasoning about mathematical structures.

Assured Development with Isabelle

Assured development with Isabelle is an approach to software or system development that emphasizes correctness and verification. Leveraging the capabilities of Isabelle, an interactive theorem prover, this process promotes reliability and robustness in software design.

Key components of this approach include:

• Formal Verification: Mathematical techniques are used to prove the properties of a system, providing a high degree of confidence that it meets its specification.

• Rigorous Testing: Alongside formal proofs, rigorous testing, such as property-based testing, is used to provide additional assurance of the system's behavior.

• Flexible Proof IDE (PIDE): Assured development with Isabelle often involves the use of the Proof IDE. This integrated development environment facilitates programming, proof development, and tool integration, providing a unified workspace for developing and verifying software.

• Machine-checked Document Model: PIDE includes a machine-checked document model with an extensible parser. This allows the system's properties and proofs to be expressed in a precise and structured way, and checked automatically for correctness.

Through these techniques and tools, assured development with Isabelle aims to produce software and systems that not only perform their intended functions but are also provably correct, substantially reducing the risk of bugs and errors.

L4. Verified in Isabelle/HOL

L4.verified is a version of the L4 microkernel that has been formally verified using Isabelle/HOL. This means that it has been mathematically proven to meet its specification, a rare achievement in real-world software development.

• proof supports the above statement: strong guarantee

Other Proof Tools
1. mathematically principled: Coq, Lean, Agda
2. highly automated: PVS
3. usable and bespoke: KeY, KeYmaera X

Theory Document Structure

In Isabelle, a "theory" is a document that contains definitions, theorems, and proofs. It is the basic unit of work. A theory document usually starts with a theory header, declaring the theory's name and its dependencies on other theories. It's followed by a series of imports, definitions, and statements (lemmas, theorems) which are either proven within the theory or left as assumptions (axioms). For instance:

theory MyTheory
  imports Main
begin

definition my_function :: "nat ⇒ nat" where
  "my_function x = x + 1"

theorem my_theorem:
  "my_function x = x + 1"
  by (simp add: my_function_def)

end

This Isabelle/HOL theory document defines a function my_function, then states and proves a theorem about this function.