Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-05-18

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

All times shown according to UTC.

Time Nick Message
00:05 mal`` joined #isabelle
01:40 Warrigal joined #isabelle
01:41 Warrigal Hey there. I'm interested in Isabelle.
01:42 _tswett Wikipedia says that Isabelle provides a weak meta-logic which is used to encode other logics such as first-order logic.
01:47 _tswett Sounds nice. The fewer axioms and rules my logical systems are based on, the better.
01:47 _tswett I haven't seen any sort of tutorial for Isabelle/Pure, though. Maybe it's best if I start with Isabelle/HOL and then move on to /Pure afterward.
01:48 ilbot3 joined #isabelle
01:48 Topic for #isabelle is now Official channel for the Isabelle/HOL theorem prover: http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html || Now with logging: http://irclog.perlgeek.de/isabelle/
02:17 keep_learning joined #isabelle
05:39 larsrh _tswett: yes, that makes sense
06:13 pruvisto _tswett: Disclaimer: Almost everyone uses Isabelle/HOL these days.
06:14 pruvisto the idea that you can do other logics with it didn't really take off that much, I would say
06:14 pruvisto Probably mainly because HOL is infinitely more usable than, say, ZF
06:15 pruvisto and developing a library of formal mathematics is a huge effort, and splitting what feeble manpower exists over two or more logics seems a bad idea
06:38 ammbauer pruvisto: why is HOL infinitely more usable than ZF?
06:44 pruvisto ammbauer: well, to be fair, I'm not an expert on this
06:44 pruvisto but that is what I heard
06:44 pruvisto part of it is the lack of a type system, i would say
06:45 pruvisto and part of it is just because of the good tooling we have in HOL
06:45 pruvisto (datatype, function, etc.)
06:45 pruvisto but I think you can have "soft types" in ZF, but I don't think we have those in Isabelle
06:45 pruvisto I think Mizar has them?
06:47 pruvisto Maybe I'm wrong about this and ZF with proper tooling is also quite usable and it's only a historic accident that HOL is so strong
06:48 pruvisto but my impression has always been that HOL is nicer to work with "out of the box" than ZF
14:50 tautologico Mizar has something like "soft types"
14:51 tautologico actually I think it's mostly a historical question... HOL is one logic, maybe better than ZF, but there are others
14:54 tautologico of course ZF by itself is not a logic, so ZF+FOL must be what's intended
14:55 tautologico isn't the semantics of HOL defined (at least as I've seen in the documentation for the HOL prover) in terms of sets?
14:56 pruvisto I'm hardly an expert on this
14:57 pruvisto but you can embed HOL into ZF in a rather natural fashion by interpreting types as sets, yes
18:08 ertes joined #isabelle
21:00 ertesx joined #isabelle
21:32 JCaesar TIL: instead of .. you can (sometimes?) write "proof qed". Looks nice and stupid. :)

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