>You can proof almost anything in agda. Even the most complicated mathematical theorems. And I think that's the thing that makes Agda interesting. If you limit

>You can proof almost anything in agda. Even the most complicated mathematical theorems. And I think that's the thing that makes Agda interesting. If you limit Agda to proving things about computer programs, it doesn't sound that special. People are using Agda to prove things about, for example, topology.