[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, 
> [..]


Before thinking of protocols, can we consider the following simple
example?
Haskell has not dependent types. But may be it still fits the goal you
name (?). To compile a function  f  that uses a function  g  from
another module, Haskell compiler uses only the signature of g given in
the interface file.

  module M1 where
  g :: Int -> Bool  
  g n = ...

  module M2 where
  import M1 (g)

  f :: [Int] -> [Bool]   
  f =  map g    

To compile f, Haskell compiler needs only the signature of  g. 
And to implement f, the programmer needs only to know the signature of
g.
Can you modify this example (a bit), so that it will become clear one
really needs dependent types?

--
SM



> 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
>