Some programming languages are, https://github.com/agda/agda
What’s the difference, compared with usual languages ? What are the applications ?
In: 1
A proof assistant help you write formal proof.
A formal proof is a kind of mathematical proof that had been written so that its validity can be checked by just checking its *form*. This is very good, because it allows a computer to check it in a mechanical manner, without having to understand what the proof means and all that. However, to have that kind of proof, a lot need to be done. All assumptions had to be written out, even obvious one, every small steps of derivations have to be written out or cited. As an analogy, if you imagine a programming language as a computer’s analog of instruction for your servants, then a formal proof is a computer’s analog of proof written for mathematicians. Just like how the computer won’t understand your intent and you have to specify everything in details when you program, the computer won’t understand the meaning of a proof and you have to write out every little details when you write formal proof.
Additionally, the kernel of the formal proof is often very low level. The kernel is the most basic level of logic that the proof operate on. At this level, formal proof is analogous to assembly language or even machine code, but even worse. To ensure that the proof-checking program actually work correctly, the kernel is very simple and lacks any features that improve efficiency. So it’s terrible to write proof at that level.
To improve efficiency, proof assistant is developed. They are partly a form of formal proof and partly an environment. If you think the kernel as analogous to assembly language, then proof assistant is analogous to a high level language together with an IDE (like Python with its command line environment). The formal proof built on top of the kernel will have features to improve efficiency. The proof assistant’s interactive interface will help you edit that formal proof more efficiently (but tbh, 99% of the usefulness of a proof assistant come from the formal proof).
Applications? To write mathematical proof in a way that you can be sure that it’s correct. This applies to both regular mathematics, as well as a programming branch of it: formal verification. In formal verification, you prove that a program you had written is correct, bug-free. Certain proof assistants are written so that it’s both a proof assistant and a programming language, so that you can write a program and prove its correctness at the same time. This is very important in certain context, such as security. A bug-free security system completely remove a huge attack vector.
Latest Answers