Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-02-08

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary

All times shown according to UTC.

Time Nick Message
09:37 dmiles joined #isabelle
10:56 silver joined #isabelle
12:53 akr joined #isabelle
12:53 akr hello
12:54 akr I'm a noob and have a few questions: (1) Is it viable to use emacs as an IDE for Isabelle? I see some official documantation, but it's kinda old, so not sure; (2) Why would I want to use Isabelle over e.g. Coq, other than unicode support? Does Isabelle have better automated theorem proving tools?
12:56 akr oh Isabelle doesn't have dependent types? :(
13:01 JCaesar 1) Hasn't been viable for… 2 years I think…
13:03 akr oh, too bad
13:06 JCaesar 3) No, doesn't.
13:14 JCaesar 2) I don't know much about Coq, so I can't really say. But from the fact that Jasmin has a project proposal to port sledgehammer to Coq, I'd say sledgehammer is better than what Coq has. Other than that, you'll probably find yourself in the situation that one system has a library for something where the other doesn't…
13:18 akr I see
13:18 akr Well, thanks a lot for taking the time to talk to me, JCaesar
13:19 JCaesar Don't worry. If you stick around for a bit longer someone else will write a WoT showing where I am wrong. ;)
13:20 akr WoT?
13:26 JCaesar Sorry. wall of text…
13:26 akr ah :)
13:55 juls joined #isabelle
15:14 chindy akr: also as you said yourself Isabelle is based on HOL and Coq is based on type theory/Dependent types. This has advantages/disadvantages, depending(heh) what you want to do.
15:18 akr chindy: can you give some typical examples of what would either be good for?
15:18 akr I only know that Agda is quite nice for various intuitionistic calculi
15:19 larsrh akr: If I were to pick a prover without knowing any prover well, I'd pick the one which has library support for the things I want to do
15:25 akr hmm, I don't think I really need any particularly huge libraries
15:25 akr maybe some topology might be nice
15:56 chindy akr: as you say yourself, Coq is intuitionistic, which is due to the fact that type theory is intuitionistic logic( for example you cannot have Law of excluded middle), as you can see in Curry howard isomorphism... Isabelle works with classical logic though
16:00 akr right
16:01 larsrh you can have the law of excluded middle in Coq
16:02 larsrh in fact there's a library you can import that adds it as an axiom
16:02 larsrh it's just that you can't extract programs from proofs if you use it
17:57 JCaesar Uh. Proving things without the LEM sounds exhausting…
17:59 pruvisto larsrh: and Coq users are much more likely to be hardcore intuitionists who refuse touching LEM
17:59 pruvisto (and of course one can do intuitionistic logic in Isabelle; but most people don't)
18:00 pruvisto (and HOL, which is by far the best-developed object logic in Isabelle, is classical)
19:00 ammbauer "not just proof-geeks who like to have a complicated and inaccesible system for their private entertainment." lol
19:04 juls joined #isabelle
19:27 larsrh https://arxiv.org/pdf/1609.07127.pdf
19:33 mbrcknl_ joined #isabelle
19:50 kyagrd joined #isabelle
20:08 stoopkid joined #isabelle
20:14 JCaesar November 2011, dafuq happened, Coq?

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary