Skip to main content
18 votes
Accepted

What difficulties are there in basing a proof assistant on the $\lambda\mu$-calculus and has any proof assistant tried?

TL; DR: There are. But there are also severe difficulties that only have unsatisfactory solutions. Let's see what bad things will happen, so we can attempt to fix it. The first thing when trying to ...
Trebor's user avatar
  • 3,967
18 votes
Accepted

What work has been done on computationally intensive proofs?

You are touching upon some questions that we are currently investigating in our research group, but we do not have definite answers yet, so let me just make a couple of comments regarding the trade-...
Andrej Bauer's user avatar
  • 9,194
15 votes
Accepted

What axioms have a computational interpretation?

This is a very broad question. Actually, it is even a whole research area, which is a major theme of what I would call the French school of type theory. Extending the Curry-Howard isomorphism from &...
Pierre-Marie Pédrot's user avatar
15 votes

What difficulties are there in basing a proof assistant on the $\lambda\mu$-calculus and has any proof assistant tried?

I think that the first question can be generalized to "What difficulties are there in adding side-effects to a proof assistant based on dependent type theory." First-class continuations are ...
Pierre-Marie Pédrot's user avatar
15 votes
Accepted

In Lean, why is the exact tactic necessary when the goal is the same as a hypothesis?

My take on that is that, in their first approximation, tactics are just ways to build terms (typically proof terms), so it is expected to have basic tactics that closely correspond to the various term ...
Joachim Breitner's user avatar
15 votes
Accepted

Any proof assistant that allows imperative computation within the language itself?

Although Lean 4 is a pure functional programming language, it is capable of expressing functions almost exactly like your example: ...
Mario Carneiro's user avatar
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,194
10 votes

Are there any proof assistants which integrate JITs?

Apart from the well-known native_compute feature of Coq, I'd like to share two JITted dependently-typed programming languages which are used for theorem proving: Lean 4: in this WITS talk, Seb said ...
ice1000's user avatar
  • 6,186
8 votes

What work has been done on computationally intensive proofs?

Not as general as Andrej's answer but more a data-point for your interest. We've been looking at how to construct formal proofs about neural network-enhanced systems in proof assistants. This runs ...
Matthew Daggitt's user avatar
8 votes
Accepted

Defining essentially unique objects with typeclasses

The question is about declarative versus computational formalization. In the declarative style we characterize a “thing” by stating conditions, quite often universal properties, that determine it up ...
Andrej Bauer's user avatar
  • 9,194
8 votes
Accepted

In the "Simply Easy!" paper, why is it safe to evaluate types in the empty environment?

All is well. The implementation distinguishes between bound variables, represented as Bound i where i :: Int and free variables, ...
Andrej Bauer's user avatar
  • 9,194
8 votes
Accepted

Have any proof assistants incorporated a notion of unsafety with Type : Type?

I will summarize the answers from the comments and add my own about Coq. Many proof assistants have a way of adding "unsafe" declarations and tracking which definitions rely on them. Coq ...
Jason Gross's user avatar
  • 1,537
7 votes

Are there any non-English based proof assistants?

The System for Automated Deduction can check proof texts both in English and Russian if I remember correctly: SAD Translating keywords is of course an easy task, but it'd be interesting to see if ...
Maximilian Doré's user avatar
7 votes

Are there any proof assistants which integrate JITs?

Coq's native_compute will invoke a modified version of ocamlc to just-in-time compile code for native evaluation. Similarly, <...
Jason Gross's user avatar
  • 1,537
7 votes

Can a theorem prover reason about its own faulty hardware?

Your claim that a theorem prover cannot prove the correctness of the hardware design it's running is not argued sufficiently carefully. Just because there could be one particular kind of CPU that is ...
Andrej Bauer's user avatar
  • 9,194
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

Why is it hard to formalize informal proofs?

Are there any theoretical obstacles in formalizing what we actually do when we mentally verify equations, etc? Yes: we don't know what we actually do when we mentally verify equations! This is a glib ...
Neel Krishnaswami's user avatar
6 votes

Probability and the de Bruijn Criterion

Do you have a source for the probability of 20 bugs for 1000 lines you give? In particular, at which stage of development does this apply? The reason I ask this is that indeed at the first iteration ...
Meven Lennon-Bertrand's user avatar
5 votes

Is there a Proof assistant that is an esoteric programming language?

Falso, by Estatis Inc. is perhaps technically an esoteric programming language, fitting into the "designed [...] as a joke" category. I've occasionally thought about how to leverage C++ ...
Jason Gross's user avatar
  • 1,537
5 votes
Accepted

How to deal with the proliferation of encodings of ASTs?

As various commenters have said, you sometimes just need to bite the bullet. Good modularity, good naming conventions and other standard good software practices will help. If you need inspiration, I'...
Michael Norrish's user avatar
4 votes
Accepted

Is it a good idea to modify the context during type checking of patterns?

I would say that having a pattern-matching construct that works differently depending on whether its scrutinee is a variable or a more complex expression sounds like a very ad-hoc thing to do. It ...
Meven Lennon-Bertrand's user avatar
4 votes

Proof assistants with dynamic scope/local instances/etc.?

Agda has generalization of declared variables. In short, you can leave a variable block of variables that are appearing often. Example: ...
Cheery's user avatar
  • 721
4 votes

Are there any non-English based proof assistants?

I point you to MMP/Geometer, by Xiao-Shan Gao. This system allows you to prove geometric theorems, even through a graphical interface. The commands on the shell are in English, the GUI is mainly in ...
M. Lonardi's user avatar
3 votes

Proof assistants with dynamic scope/local instances/etc.?

In Isabelle/Isar locale can be used to specify implicit assumptions and notation conventions that are limited in scope. The assumptions are then added to each ...
Slawomir K.'s user avatar
2 votes

What axioms have a computational interpretation?

It's not really axioms themselves that are nonconstructive it's the combination of axioms which cause issues with constructive interpretations. LEM collapses a Cartesian closed category (even ...
Ms. Molly Stewart-Gallus's user avatar

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