00:40:51 -!- ihope has joined.
01:13:40 * CakeProphet finds himself coming closer and close to making.... smalltalk
01:13:49 <CakeProphet> smalltalk with like... some added perks... and no classes.
01:14:51 <CakeProphet> syntax wise... I'm removing all the colons... and just using parenthesis... makes it look eerily lispish.
01:14:58 <ihope> Write a typed first-order logic evaluator for me. kthxbai
01:15:27 <ihope> I haven't seen one yet. Should be easy.
01:16:43 <oerjan> Assuming all your types are finite sets.
01:17:07 <oerjan> Otherwise termination is going to be a problem.
01:18:31 <ihope> If it always terminated, it wouldn't be Turing-complete.
01:18:55 <oerjan> The problem is that a forall on an infinite set would _never_ terminate.
01:19:19 <CakeProphet> a while True loop will never terminate either.
01:19:26 <oerjan> If true. Or an exists, if false.
01:19:56 <ihope> oerjan: that's where proving comes in.
01:20:20 <ihope> It doesn't take many brains to tell whether "all natural numbers are natural numbers" is true or false.
01:20:22 <oerjan> I see. And then we are getting into undecidability.
01:20:53 <ihope> 'Course, you will have to settle for undecidability in some cases. Nontermination would be fine then, eh?
01:21:46 <oerjan> Writing an evaluator that searches for proofs is "easy". Having it use a reasonable amount of time is hard.
01:39:28 -!- sebbu has quit ("Leaving").
02:14:28 -!- ihope has quit (Read error: 104 (Connection reset by peer)).
03:12:14 -!- CakeProphet has quit ("haaaaaaaaaa").
03:12:46 -!- CakeProphet has joined.
03:18:35 -!- CakeProphet has changed nick to SevenInchBread.
03:50:24 -!- calamari has joined.
04:07:32 -!- Sgeo has quit (Read error: 104 (Connection reset by peer)).
04:35:49 -!- oerjan has quit ("leaving").
04:51:17 -!- SevenInchBread has quit (Read error: 113 (No route to host)).
05:27:53 <GregorR> I've been poring it over ... and I don't think that OoU is TC, or even a BSM :(
05:40:56 -!- digital_me has quit (Remote closed the connection).
06:21:42 -!- calamari has quit ("Leaving").
06:21:45 -!- wooby has quit.
07:59:59 -!- clog has quit (ended).
08:00:00 -!- clog has joined.
08:46:46 -!- sebbu has joined.
11:36:37 <SimonRC> # For cur-- / For cur-- / For curiosity, # # Two pis-- / Two pis-- / Two pistols on my knee, # # For king-- / For king-- / For king and country, # (etc)
11:36:56 <SimonRC> Ok, maybe it works better when sung.
11:48:16 <SimonRC> argh I have a pun stuck in my head
12:44:13 -!- GregorR_ has joined.
12:44:43 <SimonRC> GregorR, GregorR_: ooh, twice the fun!
12:44:47 -!- GregorR has quit (Read error: 104 (Connection reset by peer)).
12:52:29 <oklopol> GregorR_, i proved to myself at school you can't do pretty much anything with it
12:53:49 <oklopol> i tried to find a way to get even a bit use out of the fact you can time ppl and control where they go but i can't find any even vaguely interesting things to get them to do
14:31:12 -!- tgwizard has joined.
16:30:26 <GregorR_> oklopol: Oh, you can store and retrieve data.
16:30:36 <GregorR_> So it's not utterly worthless.
16:30:41 -!- GregorR_ has changed nick to GregorR.
16:40:54 * sebbu a eu ses résultats de son 3° semestre de dut info : 5° sur 74 avec 13.597 de moyenne
17:05:14 -!- sp3tt has quit (Read error: 131 (Connection reset by peer)).
17:10:44 -!- sp3tt has joined.
19:28:57 -!- sebbu2 has joined.
19:56:04 -!- sebbu has quit (Connection timed out).
20:55:29 -!- SevenInchBread has joined.
21:21:23 -!- lament has joined.
21:55:37 -!- florian_ has joined.
21:55:49 -!- florian_ has quit (Client Quit).
22:13:27 -!- Dustfinger has joined.
22:13:39 -!- Dustfinger has quit (Client Quit).
22:19:43 -!- wooby has joined.
22:49:14 -!- digital_me has joined.
23:10:30 -!- jix__ has joined.
23:13:07 -!- sebbu has joined.
23:20:23 -!- sebbu2 has quit (Read error: 145 (Connection timed out)).
23:28:07 -!- Sgeo has joined.
23:40:49 -!- oerjan has joined.
23:46:46 -!- wooby has quit.
23:50:43 -!- jix__ has changed nick to jix.