Camelia, the Perl 6 bug

IRC log for #darcs, 2013-09-03

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

All times shown according to UTC.

Time Nick Message
00:44 gh_ joined #darcs
01:39 intripoon joined #darcs
03:28 mizu_no_oto joined #darcs
03:32 preflex_ joined #darcs
04:21 dolio joined #darcs
04:22 arpunk joined #darcs
04:32 adnap joined #darcs
05:11 preflex joined #darcs
07:01 raichoo joined #darcs
08:40 donri joined #darcs
08:59 mizu_no_oto joined #darcs
09:08 lambdabot joined #darcs
09:22 arpunk joined #darcs
11:10 mizu_no_oto joined #darcs
11:43 mami joined #darcs
11:43 mami heyho
11:44 mami are #camp and #darcs-theory defunct?
11:44 mami i see no one there
11:44 mami wanted to ask whether the camp folks thought about using idris
11:44 mami for implementation AND proving
11:44 mami or whether that is still too experimental
11:49 raichoo It would certainly be an interesting "excercise" to implement darcs' theory in Idris.
12:12 mami raichoo: do you think it would make sense at the current state of idris?
12:13 mami as in: could we use the stuff that comes out for actual work or "just" research
12:13 raichoo Not sure, but it's worth trying as an experiment.
12:13 mami k
12:13 mami have to get up to speed on idris though
12:13 raichoo To this point no one dared to write something big in idris.
13:02 bfrank_ joined #darcs
13:27 pointfree-w530 joined #darcs
13:48 mizu_no_oto joined #darcs
15:13 sm mami: yes those are probably defunct.. most eyeballs are here, better to ping Igloo here
15:14 sm I don't think #camp is darcs camp related
15:16 whaletechno joined #darcs
15:20 int-e sm: #camp of oftc may be (have not checked, but that's where the camp homepage points to)
15:22 sm ah, right you are int-e. And it's empty
15:33 arpunk joined #darcs
15:34 dolio joined #darcs
15:39 mami there is no one in #camp
15:50 raichoo joined #darcs
16:07 mizu_no_oto joined #darcs
16:34 adnap joined #darcs
17:55 byorgey mami: I tried using idris for doing some simple proofs recently, and found it to be not that usable yet
17:55 byorgey though I think it is quite usable as a programming language
17:56 byorgey I ran into weird bugs, the interactive interface didn't work very well, etc.  I never was able to prove the simple things I was trying to prove.
18:10 mizu_no_oto joined #darcs
18:56 sm wasn't Igloo working on camp with agda ?
18:57 Heffalump Coq I think
18:59 raichoo byorgey: It's getting better. I've worked through some chapters of software foundations with Idris. Turned out to work pretty well.
19:00 byorgey oh, that's great to hear
19:01 byorgey The experience I described above was a couple months ago so I wouldn't be surprised to find it's improved since then.
19:06 raichoo Anyway, there is still a lot of work to do. But it's a fun project to hack on ^^
19:07 byorgey I bet =)
19:15 mami a friend and me are going to implement some stuff for a calculus introduction
19:15 mami reporting back afterwards
19:15 mami (in idris)
19:21 arpunk joined #darcs
20:00 mizu_no_oto joined #darcs
20:21 raichoo joined #darcs
20:45 raichoo joined #darcs
21:13 intripoon joined #darcs
21:55 gh_ left #darcs
22:35 mizu_no_oto joined #darcs
23:59 mizu_no_oto joined #darcs

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