[Agda] Do you use postulates extensively?

[Apostolis Xekoukoulotakis]

The need for dependent types arises because in most cases, we need to
describe exactly what a function does, and other type systems are not
sufficient.
For example the function g could be implemented by randomly selecting true
or false per int number.

A more concrete example is agda's Defn(1) definition. There, many of the
Maybes depend on the current stage of the computation. The comments play
the role of telling the programmer what to expect.
In many cases , comments are missing, or are wrong because you forget to
update them. Moreover, to understand the comments, you need to understand
the order of the computation. In other words,
you need to learn many parts of the agda code , to simply use a data
structure. This type of programming cannot scale. It can only work for a
very small group of people, and for a very small code base.

With a refinement of a protocol, I actually mean the refinement as is
described in TLA+(2). The arguments are the same as in the previous case.
The difference is that now , the group of people that change parts of the
protocol / the application
are so many that it is impossible to coordinate them, you might not even
know they exist.

On another note, there are very important positive results if we only use
the type to determine if a function is correct. Developers are free to use
different implementation and this induces an evolutionary process similar
to organisms.
Mutations of a protein can exist as long as the functionality remains the
same.(3)

(1) :
https://github.com/agda/agda/blob/master/src/full/Agda/TypeChecking/Monad/Base.hs#L1656
(2) : https://lamport.azurewebsites.net/tla/tla.html
(3) : http://hal.elte.hu/fij/r/b/dsc/Hartwell.pdf

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

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