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
6 votes
2 answers
120 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 ...
user avatar
  • 2,688
8 votes
1 answer
160 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 ...
user avatar
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 ...
user avatar
14 votes
2 answers
243 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 ...
user avatar
19 votes
2 answers
316 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 ...
user avatar
11 votes
2 answers
106 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 ...
user avatar
12 votes
1 answer
185 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: ...
user avatar
  • 363
11 votes
1 answer
143 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 ...
user avatar
  • 671
19 votes
1 answer
242 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 ...
user avatar
10 votes
1 answer
109 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 ...
user avatar
  • 664
6 votes
1 answer
108 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 ...
user avatar
  • 1,409
-4 votes
1 answer
133 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?
user avatar
16 votes
2 answers
162 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 ...
user avatar
  • 671
11 votes
2 answers
208 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 ...
user avatar
13 votes
2 answers
168 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 ...
user avatar
  • 566
10 votes
1 answer
141 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, ...
user avatar
  • 423