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.

Filter by
Sorted by
Tagged with
1 vote
0 answers

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 &...
Eric Anderson's user avatar
10 votes
2 answers

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 ...
Matthias Georg Mayer's user avatar
5 votes
2 answers

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 ...
nicolas's user avatar
  • 183
5 votes
1 answer

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 ...
Trebor's user avatar
  • 3,688
5 votes
0 answers

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

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 ...
Will Sawin's user avatar
5 votes
1 answer

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 ...
Greg Nisbet's user avatar
  • 2,711
27 votes
8 answers

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

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

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. ...
Agnishom Chattopadhyay's user avatar
16 votes
7 answers

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?
taylor.2317's user avatar
  • 1,308