[Agda] Do you use postulates extensively?

[Apostolis Xekoukoulotakis]

I use agda as a programming language. So the computational path is the part
of the program that will be executed.

For me , agda will help to decentralize the development of software. If the
types describe a function accurately enough, one can replace one
implementation with another without the need to coordinate with the other
developers.
In fact, each developer only needs to know the type and nothing about the
other parts of the software.

Now, if we extend this idea to the development of network protocols, we can
have an abstract protocol, and developers refining parts of it.
In that way, we have the concurrent evolution of network protocols without
the need for a coordination mechanism which in this case , it is very
difficult to have.

I do not see any other way to do this . So for me , agda is indispensable .

On Fri, Jan 18, 2019 at 1:36 PM Sergei Meshveliani <mechvel at botik.ru> wrote:

> 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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190118/356da7d0/attachment.html>