Thinking about learning Agda? Think again.
13 plus ones
Shared publicly•View activity
View 3 previous comments
- http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdfI usually recommend that people start by reading 's Agda tutorial from a couple of years ago:
Unfortunately, there are a few minor issues in the pdf (Ulf, is the TeX source up anywhere for us to try fixing?) so I'd also recommend coming to the painfully helpful #agda IRC channel on freenode :)Jan 30, 2012
- Having used Isabelle for my work, I can say I have a marked preference for Agda over something as messy as Isabelle. Isabelle's proofs are easier to write, but much harder to read. Also, Isabelle's proof language and term language are entirely separate (because it's not dependently typed) so you can't do many cool tricks that you can do in Agda by mixing proofs and code. Proofs also cannot be structured in much detail beyond locales (which are slow) or theories (which aren't real modules). Finally, Isabelle/HOL's FP modelling language is very limited (type classes on one *-kinded constructor only?) and has awkward precedence syntax, which makes it quite frustrating to program in. Agda on the other hand makes a very expressive programming language as well as a proof language (they're the same) so you can use all the same abstraction techniques that you can use for code for proofs.Jan 30, 2012
- Isabelle's simplifier is substantially more powerful than what that tutorial is referring to. There is no magic rewrite system in Agda.Jan 31, 2012
- Guess what's taped on the back of my chair since a couple of days? Thanks(and my dear officemates)!Feb 6, 2012
- I hope it didn't come across as mocking! I think your code is very impressive, and would love to see it used/documented more!Feb 6, 2012
- I really liked the joke! ;)
Last time I tried to work on the solver, typechecking time was the main problem: the smallest modification takes ages to check.
Concerning the lack of documentation: the technique used follows closely Chaied & Nipkow's "Proof synthesis and reflection for linear arithmetic" (2008). This is probably the best way to understand what is happening (apart from reading the source files, obviously :D).Feb 7, 2012