Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-08-13

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

All times shown according to UTC.

Time Nick Message
01:51 ilbot3 joined #isabelle
01:51 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/
04:52 stoopkid_ joined #isabelle
07:32 int-e joined #isabelle
09:45 chuchucorny int-e: thx
18:03 pruvisto chindy: "_ > 0" seems needlessly strong
18:03 pruvisto certainly, _ ? 0" will suffice
18:03 pruvisto I'll look into it
18:04 pruvisto unless I forget
18:04 chindy good point
18:04 pruvisto in which case you can feel free to remind me ^^
18:04 chindy :)
18:05 pruvisto chuchucorny: honestly I don't really see the point
18:05 pruvisto why set up I/O stuff in Isabelle if you can't reason about it?
18:08 chindy can someone explain why a known possibilty to derive False, does not seem to be a big enough problem to fix it? (the word64 bug in sml 5.6)
18:09 larsrh chindy: it requires custom setup to be triggered
18:09 larsrh 'eval' is always prone to these problems
18:09 larsrh i.e. it is trivial you can make custom setup
18:09 larsrh err
18:09 larsrh i.e. it is trivial to make custom setup that derives 'False'
18:10 larsrh even without exploiting compiler bugs
18:21 chindy does eval work with oracles?
18:27 larsrh yep
18:27 larsrh it generates code from the current goal and checks whether that evaluates to True
18:29 chindy larsrh: i see... and the "proofs" from oracles dont go through the kernel?
18:29 larsrh nope
18:29 larsrh they only get typechecked, that's it
18:30 chindy but metis/smt/... go through the kernel, right?
18:31 larsrh yes
21:55 chindy also: http://downthetypehole.de/paste/5NJWfWkp
21:55 chindy would be nice if this could be added to GCD

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