[Agda] Do you use postulates extensively?

[Sergei Meshveliani]

On Wed, 2019-01-16 at 16:01 +0200, Apostolis Xekoukoulotakis wrote:
> Mathematics has used informal proofs for thousands of years, and this
> is why we made progress because the cost of a formal proof is
> enormous.

The cost of each new formal proof is reduced greatly when one uses a
large library of theorems proved formally earlier, when this library is
designed for the corresponding subject domain. This is similar as with
humanly proofs. 
One accumulates a library during a couple of years, and then one feels,
that formal proofs become easier.

Still the cost remains great.


> Why then use agda?


So far I see only the four reasons.
(1) Dependent types support an adequate domain representation in  
    mathematics -- apart from possibility of formal proofs.
 
(2) Informal proofs often have mistakes (I have shown an example 
    earlier).

(3) For curiosity: to play with formalism, to see which theorems can in 
    reality be proved formally, what resource will it take.
    For what aim, I do not know. 

(4) A proof design in Agda is an important area of application for 
    automatic provers. The more powerful prover is the more proof 
    assistance Agda will provide when a program uses this prover in its 
    library. So far, provers save may be 2% of the proof composing 
    effort. But they have to progress.


>  Because types can guide the implementation of parts that are
> important or are part of the computational path.


Without example, this is difficult to understand (for me).

Regards, 

--
SM