[Agda] Do you use postulates extensively?

[Sergei Meshveliani]

On Fri, 2019-01-18 at 16:43 +0200, Apostolis Xekoukoulotakis wrote:
> 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 .



I do not know any about network protocols. To "refine a part of an
abstract protocol" (whatever this might mean), the developer, may be,
needs be given a specification of the properties of the arguments and of
the properties of the function to be programmed. Is this so?
Suppose, one writes this function in Haskell, and writes so that the
function to satisfy the given specification. And where are dependent
types?

--
SM