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, as the name suggest, is some language or framework that can assist you in finding or developing proofs of something, usually mathmatical theorems.
So the human would use the language to guide the search for proof, and the computer would then run trough the heavy computation needed to verify or exhaust some search space. It’s kind of like a more advanced calculator: a programming language whose entire job is to be used to write and find proofs for logical statements.
Latest Answers