Personal site of Dominik Wójt

This page is read only. You can view the source, but not change it. Ask your administrator if you think this is wrong.
====== Formal systems ======

By formal system I mean a language for expressing statements, rules to prove them and usually a reference computer program, which verifies those proofs.

===== Metamath =====

[[http://us.metamath.org]]

Probably the simplest system being able to prove all the mathematics one can learn up to high school.
Based on principle of rewriting with substitution.

===== Mizaar =====

[[http://mizar.org/]]

A system with focus on syntax resembling usual mathematical notation.

===== Coq =====

[[https://coq.inria.fr/]]

One of the more modern systems.
It is based on intuitionistic approach.
It strongly relies on Curry-Howard principle and is a great way to understand that principle.
In my opinion, the best source to start learning it is first volume of [[https://softwarefoundations.cis.upenn.edu/|software foundations]].

==== Notable developments ====

Correctness of C compiler [[https://compcert.org/compcert-C.html|CompCert]] was proven with Coq.

[[https://deepspec.org|DeepSpec]] is an expedition to formally specify and provide verified implementations for basic computer systems. The subjects covered are C compiler, micro kernel, CPU instruction set and hardware implementation.

Coq has been used to prove some properties of [[https://hedera.com/blog/coq-proof-completed-by-carnegie-mellon-professor-confirms-hashgraph-consensus-algorithm-is-asynchronous-byzantine-fault-tolerant|Hedera hash graph algorithm]].

===== HOL/Isabelle =====

Somewhat similar to Coq. Has strong emphasis on automated proof finding.

[[https://isabelle.in.tum.de/]]

==== Notable developments ====

Correctness of [[https://sel4.systems/|seL4]] microkernel was proven with HOL.