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.
19
questions
1
vote
0
answers
113
views
Designing a proof assistant around Cubical
As far as I know, Agda is currently the only "widely popular" theorem prover to have somewhat good HoTT support via it's CubicalTT mode. Now, I understand what has slowed down the addition ...
- 111
4
votes
1
answer
273
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 ...
- 41
4
votes
1
answer
76
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,877
6
votes
2
answers
186
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,688
8
votes
1
answer
173
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 ...
- 2,768
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 ...
- 495
16
votes
2
answers
352
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 ...
- 1,015
19
votes
2
answers
439
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 ...
- 829
11
votes
2
answers
117
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 ...
- 211
12
votes
1
answer
454
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
168
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 ...
- 681
20
votes
1
answer
322
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 ...
- 829
10
votes
1
answer
167
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
137
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,459
-4
votes
1
answer
147
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?
- 245
15
votes
2
answers
198
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 ...
- 681
10
votes
2
answers
233
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 ...
- 400
12
votes
2
answers
197
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
11
votes
1
answer
159
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, ...
- 495