Skip to main content
17 votes
Accepted

Can the language of proof assistants be used for general purpose programming?

There are many types of proof assistants using many types of foundations. While all of them resemble "code", in the same way that $LaTeX$ or HTML resembles code, most of them don't resemble ...
Jason Rute's user avatar
  • 8,655
12 votes

Can theorem provers be used to form foundations for programming languages?

If you are asking "can we use proof assistants to develop foundations of programming languages" then the answer is positive. Two well-known such developments are: Software foundations by ...
Andrej Bauer's user avatar
  • 9,104
7 votes

Can theorem provers be used to form foundations for programming languages?

I'm interested in this application of theorem provers, but it's not my speciality. I can point you to Harper and Licata's paper Mechanizing Metatheory in a Logical Framework, which walks through using ...
Alex Nelson's user avatar
  • 1,564
6 votes
Accepted

How can you represent a dependent type visually?

I addressed some of these questions in my lecture “Spartan Type Theory” (PDF slides) at the UniMath 2017 school in Birmingham. In particular, slide 18 looks like this: Please look at the slides for ...
Andrej Bauer's user avatar
  • 9,104
6 votes
Accepted

Do implementations of a PA and of ATP have overlap?

Unfortunately there is much less code reuse possible than one would hope. There three levels to consider: Differences between mathematical foundations (and implementations) between proof assistants. ...
Anja Petković Komel's user avatar
6 votes

Can the language of proof assistants be used for general purpose programming?

I just want to add a couple of minor footnotes to an excellent answer by Jason Rute First of all there's no "the language" of proof assistants — pretty much every proof assistant implements ...
Alex Chichigin's user avatar
5 votes

Using proof assistants to generate fast code

I would say that this paper, with code in Coq, meets your requirement: Verified tensor-program optimization via high-level scheduling rewrites First two sentences of the abstract We present a ...
tom's user avatar
  • 221
4 votes

Are there minimal typed proof verifiers that can deal with the majority of mathematics?

It is hard to give an answer without knowing your use case. But it is fairly easy to make a minimalist HOL theorem prover. The axioms of HOL are quite simple. HOL-light is actually fairly ...
Jason Rute's user avatar
  • 8,655
3 votes

Proof Assistants in OOP languages

The historic reason why most proof assistants are implemented in functional languages is that ML (predecessor to Standard ML and OCaml) was invented to implemented the LCF proof assistant which ...
Alex Nelson's user avatar
  • 1,564
3 votes
Accepted

Proof Assistants in OOP languages

There are many competing concerns when it comes to what languages to use to build a proof assistant. What is a proof assistant? A modern proof assistant is actually many parts put together. The most ...
Jason Rute's user avatar
  • 8,655
3 votes

Using proof assistants to generate fast code

I think your question can be interpreted in many different ways. Since you tagged it with coq, lean, and agda (initially), I assume you are interested in dependent type theory. DTT is special in ...
Jason Rute's user avatar
  • 8,655
3 votes

Can the language of proof assistants be used for general purpose programming?

You say "language" but really most proof assistants support multiple languages. You would want at least one language to write your algorithm in and another language to write your proofs in. ...
Ms. Molly Stewart-Gallus's user avatar
3 votes
Accepted

How does Lean4 (or a typical PA) represent lambda functions or in other words arbitrary expressions?

(This answer assumes you already know some of the basics of Lean as in Theorem Proving in Lean 4.) In a typical first logic class or set theory class in college, first order logic is presented as ...
Jason Rute's user avatar
  • 8,655
2 votes
Accepted

How do you implement what's in the Pierce Book precisely? And why / why not have evaluation just mutate ParseTree's of a PEG parser generator library?

Faithfully implementing textbook small-step semantics is not necessarily the best way to implement an interpreter. Large step semantics is often more intuitive and direct, as it amounts to a ...
Andrej Bauer's user avatar
  • 9,104
2 votes

Proof Assistants in OOP languages

Here are three that are implemented in non-functional languages: Arend is implemented in Java. Lean 3 is implemented in C++. Metamath has verifiers implemented in C, Rust, Javascript, Mathematica, ...
Andrej Bauer's user avatar
  • 9,104
2 votes
Accepted

Can Coq grab some data over HTTP and then write the data as declartions in Coq itself?

Naïvely, the answer is no: Coq's programming language is not effectful, meaning in particular that there is no way to do input-output, either over http and otherwise. As you remark, there is a ...
Meven Lennon-Bertrand's user avatar
2 votes

Are there minimal typed proof verifiers that can deal with the majority of mathematics?

Everything is almost trivial to implement if you strip it to bare bones. The Calculus of Constructions --- or more generally, pure type systems --- can be implemented in 100 lines of code, and if you ...
Trebor's user avatar
  • 3,927
2 votes

Proof Assistants in OOP languages

Because logic is a functional programming language The point of a proof assistant isn't to write programs, it's to write proofs. For example, consider proving the statement $A \implies (B \implies A)$....
Christopher King's user avatar
1 vote

How to find the data type of a Json value that in lean4, to perform type validation. (Functional programming in lean)

Lean's built-in JSON functionality allows you to do two main things: Convert a JSON string into the type Json. Once in this type, you can do any sort of checks ...
Jason Rute's user avatar
  • 8,655

Only top scored, non community-wiki answers of a minimum length are eligible