Which proof assistant do you recommend?

### Daniel Peebles

Shared publicly -Thinking about learning Agda? Think again.

13

4

11 comments

This is from an impressive verified Presburger arithmetic solver (Cooper's algorithm) in Agda, and I mean no offense to its original author :) It's just a rather large wall o' code (there's a lot more than I included in the screenshot!)

Daniel Peebles

+

2

3

2

3

2

+Shae Erisson I actually love Agda :) this post was mostly a joke about how terrifying a large proof can be

+Shae Erisson You might want to try Isabelle/HOL, although they differ significantly, at least from what I can see superficially.

+Daniel Peebles For someone who wants to extend his horizon, how do you recommend learning Agda?

+Daniel Peebles For someone who wants to extend his horizon, how do you recommend learning Agda?

+Lars Hupel I usually recommend that people start by reading +Ulf Norell's Agda tutorial from a couple of years ago: http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf

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

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

+Lars Hupel 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.+Liam O'Connor Yes, I'm aware of many shortcomings of Isabelle/HOL. It struck me as odd that it is not possible to model Applicatives or similar concepts easily. It also seems that there is only little hope that this will be changed. However, I don't agree with you about proof structuring. I found Isar to be really usable and after some experience, it is possible to write human-readable proofs with it.

After having a look into the paper +Daniel Peebles linked to, I have some questions. It was stated that some "trivially" true propositions can be proven automatically by the type checker. How does that compare to Isabelle's simplifier? In practice, how often do you have to spell out minor proof steps?

(Fun fact: When searching for a comparison between both systems, I found nothing substantially except people talking about whether "Isabelle" or "Agda" are nice first names.)

After having a look into the paper +Daniel Peebles linked to, I have some questions. It was stated that some "trivially" true propositions can be proven automatically by the type checker. How does that compare to Isabelle's simplifier? In practice, how often do you have to spell out minor proof steps?

(Fun fact: When searching for a comparison between both systems, I found nothing substantially except people talking about whether "Isabelle" or "Agda" are nice first names.)

Isabelle's simplifier is substantially more powerful than what that tutorial is referring to. There is no magic rewrite system in Agda.

Guess what's taped on the back of my chair since a couple of days? Thanks +Daniel Peebles (and my dear officemates)!

+guillaume allais 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!

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

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

Add a comment...