<div dir="ltr"><div>I use agda as a programming language. So the computational path is the part of the program that will be executed.</div><div><br></div><div>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. <br></div><div>In fact, each developer only needs to know the type and nothing about the other parts of the software.</div><div><br></div><div> Now, if we extend this idea to the development of network protocols, we can have an abstract protocol, and developers refining parts of it.</div><div>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.</div><div><br></div><div>I do not see any other way to do this . So for me , agda is indispensable .<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, Jan 18, 2019 at 1:36 PM Sergei Meshveliani <<a href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">On Wed, 2019-01-16 at 16:01 +0200, Apostolis Xekoukoulotakis wrote:<br>
> Mathematics has used informal proofs for thousands of years, and this<br>
> is why we made progress because the cost of a formal proof is<br>
> enormous.<br>
<br>
The cost of each new formal proof is reduced greatly when one uses a<br>
large library of theorems proved formally earlier, when this library is<br>
designed for the corresponding subject domain. This is similar as with<br>
humanly proofs. <br>
One accumulates a library during a couple of years, and then one feels,<br>
that formal proofs become easier.<br>
<br>
Still the cost remains great.<br>
<br>
<br>
> Why then use agda?<br>
<br>
<br>
So far I see only the four reasons.<br>
(1) Dependent types support an adequate domain representation in  <br>
    mathematics -- apart from possibility of formal proofs.<br>
<br>
(2) Informal proofs often have mistakes (I have shown an example <br>
    earlier).<br>
<br>
(3) For curiosity: to play with formalism, to see which theorems can in <br>
    reality be proved formally, what resource will it take.<br>
    For what aim, I do not know. <br>
<br>
(4) A proof design in Agda is an important area of application for <br>
    automatic provers. The more powerful prover is the more proof <br>
    assistance Agda will provide when a program uses this prover in its <br>
    library. So far, provers save may be 2% of the proof composing <br>
    effort. But they have to progress.<br>
<br>
<br>
>  Because types can guide the implementation of parts that are<br>
> important or are part of the computational path.<br>
<br>
<br>
Without example, this is difficult to understand (for me).<br>
<br>
Regards, <br>
<br>
--<br>
SM<br>
<br>
</blockquote></div>