What are some examples of proofs that are also themselves "useful" programs?

Question

With dependent types, types can be statements that are true or false and constructing a value with that type constitutes a proof of that statement. This proof/value construction is itself a program that can be run (which I think encapsulates the Curry-Howard Equivalence idea), but often these programs are not very "useful". For example, consider the following type statement:

(Π ((n Nat))
  (= Nat (sum_of_first_n_nat n) (n*(n+1)/2))
)

Which claims that for all natural numbers, some primitive-recursive function sum_of_first_n_nat will always give the same answer as that closed-form formula for finding the sum of the first n natural numbers. A proof of this would probably use induction and, although would likely also yield the actual answer when given a concrete n value, would compute it somewhat inefficiently - iterating over all the natural numbers up to n instead of using the closed form solution.

Are there any well-known examples of dependent-type proofs that are themselves useful programs? Of the sorts of statements that humans would like to prove when writing programs, what proportion could likely be given "useful" proofs? Is it often possible to make a proof "useful" given sufficient creativity and effort, or is this highly dependent on what the statement is? Is having all proofs be useful a desirable goal when writing a dependently-typed program?

Answer 1

Many constructive proofs could be useful. For example, to prove that every set of points in the plane (in general position) have a Delaunay triangulation, you would give the algorithm for producing the Delaunay triangulation, along with a proof that the result of the algorithm satisfies the desired properties. In pseudo-code the type signature of this proof might look like:

points-in-general-position -> (triangulation-of-those-points, proof-that-this-is-a-Delaunay-triangulation)

So just using the first value in the output pair would give you the desired value. Though another way to phrase this would make the proof 'useless': you could first write the algorithm as one function and then prove a proposition that the result of the algorithm is always a Delaunay triangulation. This separates out the useful computation part from the proof part.

Another example would be proving that a set with some binary operator is a group. If done constructively, that would involve giving an explicit algorithm for the inverse of any element, which may be quite nontrivial.

Answer 2

I guess it largely depends on how you define "useful"?

Here is a proof of a sorting algorithm: https://blog.adacore.com/i-cant-believe-that-i-can-prove-that-it-can-sort