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
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 &...
Eric Anderson's user avatar
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 ...
Matthias Georg Mayer's user avatar
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 ...
nicolas's user avatar
  • 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 ...
Trebor's user avatar
  • 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 ...
ice1000's user avatar
  • 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 ...
Will Sawin's user avatar
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 ...
Greg Nisbet's user avatar
  • 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, ...
wizzwizz4's user avatar
  • 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. ...
Agnishom Chattopadhyay's user avatar
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?
taylor.2317's user avatar
  • 1,308