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 bestdeveloped object logic in Isabelle, is classical) 
19:00 
ammbauer 
"not just proofgeeks 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? 