Questions tagged [design]

Use this tag when a question is related to specifics on how a proof assistant works. Do not use this tag for questions related to using a proof assistant.

Filter by
Sorted by
Tagged with
4 votes
1 answer
244 views

Why is it hard to formalize informal proofs?

Say I have some informal but rigorous argument in line with eg real analysis. Currently, it is a massive PITA to do algebraic manipulations in proof assistants like Coq or Isabelle. However, in ...
4 votes
1 answer
74 views

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

So I'm working on type checking of an expression that pattern matches on terms, like case x of in Haskell. My question is, suppose we have ...
  • 5,374
6 votes
2 answers
173 views

Defining essentially unique objects with typeclasses

I noticed that in Lean, the localization of rings (which is unique up to isomorphism) is defined as a predicate is_localization. I am not an expert in Lean, and I'm ...
  • 3,143
8 votes
1 answer
165 views

How to deal with the proliferation of encodings of ASTs?

When working with type theory and ASTs one often ends up with a large amount of different encodings. It's very similar to the same problem in compiler design but more annoying because it's dependently ...
31 votes
2 answers
2k views

What work has been done on computationally intensive proofs?

Fifty years ago, few would have imagined that the process of verifying the correctness of a known proof of a mathematical theorem might be so costly that the mathematical community would hesitate to ...
15 votes
2 answers
284 views

What axioms have a computational interpretation?

The type of call/cc (which may be realized with the 𝜆𝜇-calculus) corresponds with Peirce's Law, which implies LEM. This answer by Pierre-Marie Pédrot explains how ...
19 votes
2 answers
378 views

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

The $\lambda\mu$-calculus is a variant of the $\lambda$ calculus introduced by Parigot to capture classical logic. The Wikipedia article describing it in more detail is here. In modern proof ...
11 votes
2 answers
112 views

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

Say I'm formalizing something in group theory, and I'm working with some action $\cdot$ of $(G, +)$ on a set. In my math textbook, the identity of $\cdot$ is explicitly mentioned once (if that), and ...
12 votes
1 answer
240 views

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

In Lean, when proving basic theorems, one runs into the following kind of thing: ...
  • 363
11 votes
1 answer
161 views

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

The paper in question: An Implementation of a Dependently Typed Lambda Calculus by Andres Löh, Conor McBride and Wouter Swierstra. I'm wondering whether it's correct in what's it is doing. Precisely ...
  • 671
19 votes
1 answer
281 views

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

Many proof assistants start with the notion of $Type : Type$ which is inconsistent. This choice makes type checking and some natural recursions arguably easier. Of course, universe levels can be added ...
10 votes
1 answer
131 views

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

To my knowledge, the well-known ones like Coq, Agda, Lean are all purely functional languages, and therefore require any computational function to be written in lambda calculus style. For example, you ...
  • 674
6 votes
1 answer
117 views

Probability and the de Bruijn Criterion

Background: definition of de Bruijn Criterion. Henk Barendregt coined the term "the de Bruijn criterion", which seems variously defined as: It was emphasised by de Bruijn that in case of ...
  • 1,439
-4 votes
1 answer
141 views

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

Is there a Proof assistant which also is an esoteric programming language? If so, then how many there are, approximately?
16 votes
2 answers
182 views

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

I started programming a Haskell-clone recently (source code). After basic hindley-milner, problems start to arise. Implementation of data/codata statements seem to ensure my language is breaking up on ...
  • 671
11 votes
2 answers
216 views

Are there any non-English based proof assistants?

There is a Wikipedia article about non-English based programming languages, but what about for proof assistants? I recall seeing one which was a translation of Lean tactics to French, by Patrick ...
13 votes
2 answers
183 views

Are there any proof assistants which integrate JITs?

Has there been notable research or attempts to integrate a JIT compiler into a proof assistant in order to achieve performance gains for proof verification, or general programming? Whilst it may seem ...
  • 566
12 votes
1 answer
150 views

Can a theorem prover reason about its own faulty hardware?

Most proof assistants assume that their hardware is correct. However, there are many recorded instances of CPUs outputting incorrect answers for various calculations (especially, but not limited to, ...
  • 443