[Agda] Blog post about agda2hs

[mechvel at scico.botik.ru]

On 2022-10-06 12:29, Jesper Cockx wrote:
> Hi Agda folks,
> 
> I've just published a new blog post about agda2hs, a tool that
> originated from some of the previous Agda meetings and we recently
> presented at the Haskell Symposium. You can read the post here:
> https://jesper.sikanda.be/posts/agda2hs.html. I'm very curious to hear
> if you have any ideas or applications of the tool!
> 


Jesper,

you write there
"
Sadly, in industry many people are forced to work in languages with a 
weak type system, such as Haskell.
What should you do in such a situation? Quit your job? Give up and 
despair?
Perhaps, but I have another suggestion that I’d like to explain in this 
post: use our tool agda2hs.

What is this agda2hs, I hear you asking? Agda2hs is a tool for producing 
verified and readable
Haskell code by extracting it from a (lightly annotated) Agda program. 
This means you can write
your code using Agda’s support for dependent types, interactive editing, 
and termination checking,
and from this agda2hs will generate clean and simply typed Haskell code 
that looks like it was written
by hand. Your boss will be amazed that all of your code is correct from 
the first try, and never even
suspect that you secretly proved its correctness in Agda!
"


It depends on the desired level of verification.

Most of the methods, that are programmed in Haskell in 5 days cannot be 
programmed
in Agda as a totally verified program, say, in 50 days.
Often it is more practical to write a Haskell program, to supply it with 
a non-formal proof,
and to test it on examples. This takes many times less effort than total 
verification.

But if the goal is a totally verified program (probably a rare case in 
industry, it costs much),
then yes, the idea looks all right.

Another question is performance. How often the program obtained by
problem -> Agda -> Haskell
runs many times slower than the one originally written in Haskell?
(mainly, I mean GHC).

Probably, people needs to try examples.
Also what about proofs internally accumulated in the function body and 
being returned
as a part of the result? Many methods cannot be in practice programmed 
in Agda in another way.
A contrived example:
   gcd  for Nat  written in Agda, with accumulating recursively a proof 
in its body.
And  gcd! a b =  proj1 (gcd a b)

that chooses the proper gcd value.
How will it look the converted Haskell program for  gcd! ?

Regards,

------
Sergei