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?