Questions tagged [applications]
Use this tag when the question is about using a Proof Assistant for a purpose, how would you apply the Proof Assistant to solve a particular problem. Do not use this tag if it relates to a software application. Do not use this tag to ask about apps.
11
questions
1
vote
0
answers
58
views
Embedding proof assistance in an application
Context
Perhaps this is too open-ended a question for StackExchange, in which case I apologize, but otherwise here goes:
I have a project I'm toying around with, the core of which is what I'd call &...
- 111
10
votes
2
answers
2k
views
How can we formalize a game where each player is a program having access to opponent's code?
How can we define in a proof assistant (eg., Coq) a notion of a 2-player game, where each player is a program that has access to the opponent's source code?
Background: In Open Source Game Theory, we ...
5
votes
2
answers
999
views
Using proof assistants to generate fast code
Proof assistants allow to state that
$$A(BC) = (AB)C$$
with $A$,$B$,$C$ compatible matrices,
Is there a formal system that takes this sort of equations to choose among interpretation strategies of ...
- 183
5
votes
1
answer
172
views
Application of `SSet` in Agda
Is there any presentable work that makes essential use of SSet in Agda? I kind of get the theory, but I'm not sure about the practical value of this. The ...
- 3,688
5
votes
0
answers
1k
views
What's the general idea (intuition) behind Andrej's topos where reals are countable? [closed]
I am very surprised that Andrej Bauer claimed to have found a topos where reals are countable. He said it'll take a month to write down the proof, and I think that's very understandable.
However, I'm ...
- 5,877
14
votes
4
answers
305
views
Algorithms obtained through constructive formalization
Formal proofs in proof systems that avoid the law of the excluded middle and certain other principles can be automatically converted into algorithms.
What useful new algorithms have been produced by ...
- 891
5
votes
1
answer
127
views
Libraries of formally stated theorems with proofs verified by humans
This answer by Kevin Buzzard talks, among other things, about incremental progress made in Lean's mathlib vs Isabelle.
There's a lot in that answer that I don't understand, but one thing that seems ...
- 2,711
27
votes
8
answers
728
views
Where can I find lists of theorems that have been verified?
I recall many years ago seeing a very large and well-interlinked (by computer) list of verified results starting from base assumptions and leading to all sorts of things that naive me did not expect ...
18
votes
2
answers
294
views
How can I prove facts about floating point calculations?
In computing, there is a standard called IEEE 754. Unlike in mathematics, computers have to fit numbers into a finite amount of space; to do this, they use a format a bit like scientific notation, ...
- 495
14
votes
4
answers
258
views
Proof Assistants with support for creating executable software artifacts
I am looking for proof assistants with which I can write sound proofs about my functions and values, as well as compile actions of type IO () into executable code. ...
- 1,241
16
votes
7
answers
812
views
What are some examples of proof assistants doing something useful? [closed]
I know that Proof Assistants can be used in fact-checking, but what else can they be used for? How would they be used for specific roles, including industry jobs and everyday life?
- 1,308