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
1 vote
0 answers

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 ...
blueberry's user avatar
  • 111
4 votes
1 answer

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 ...
user2013's user avatar
4 votes
1 answer

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 ...
ice1000's user avatar
  • 5,877
6 votes
2 answers

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 ...
Trebor's user avatar
  • 3,688
8 votes
1 answer

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 ...
Molly Stewart-Gallus's user avatar
31 votes
2 answers

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 ...
Timothy Chow's user avatar
16 votes
2 answers

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 ...
James Martin's user avatar
  • 1,015
19 votes
2 answers

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 ...
Andrew Marmaduke's user avatar
11 votes
2 answers

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 ...
Joshua Grosso's user avatar
12 votes
1 answer

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: ...
march's user avatar
  • 363
11 votes
1 answer

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 ...
Cheery's user avatar
  • 681
20 votes
1 answer

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 ...
Andrew Marmaduke's user avatar
10 votes
1 answer

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 ...
Bubbler's user avatar
  • 674
6 votes
1 answer

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 ...
Alex Nelson's user avatar
  • 1,459
-4 votes
1 answer

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?
Fmbalbuena's user avatar
15 votes
2 answers

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 ...
Cheery's user avatar
  • 681
10 votes
2 answers

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 ...
Jia Ming جيا ميڠ's user avatar
12 votes
2 answers

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 ...
Julian's user avatar
  • 566
11 votes
1 answer

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, ...
wizzwizz4's user avatar
  • 495