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
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 ...
4 votes
2 answers
958 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 ...
  • 149
5 votes
1 answer
146 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,261
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,424
14 votes
4 answers
286 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 ...
5 votes
1 answer
122 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,651
27 votes
8 answers
568 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 ...
17 votes
2 answers
214 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, ...
  • 443
14 votes
4 answers
212 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. ...
16 votes
7 answers
730 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,258