[Agda] New blog post: Formalize All the Things (in Agda)

[mechvel at scico.botik.ru]

On 2019-10-07 15:01, Jesper Cockx wrote:
> Hi Agda people,
> 
> I wrote a new blog post on formalizing things in Agda:
> https://jesper.sikanda.be/posts/formalize-all-the-things.html I hope 
> you find it useful. It is meant to be an
> introductory post, so let me know if there's anything that can be 
> clarified!


The main point to explain to a beginner is: why Agda instead of Gallina 
+ Coq ?

This explanation is needed because Coq is elder and widely known, and 
has a much larger functionality in libraries.
Personally, I know almost nothing about Gallina and Coq, and cannot name 
anything besides
* pure functionality and lazy evaluation by default. And this is only a 
matter of a taste.
* As to an additional language for proofs, I do not find its necessity 
in Agda, so far.
   But I do not know how will it be when some generic prover will be 
started to really assist composing proofs.
* Is Agda really better in programming ordinary evaluation?
   What about efficient implementation for ordinary programs, about the 
run-time performance?

Regards,

------
Sergei