00:40:51 -!- ihope has joined. 01:13:40 * CakeProphet finds himself coming closer and close to making.... smalltalk 01:13:49 smalltalk with like... some added perks... and no classes. 01:14:26 Smalltalk, eh? 01:14:35 It's pretty neat. 01:14:51 syntax wise... I'm removing all the colons... and just using parenthesis... makes it look eerily lispish. 01:14:58 Write a typed first-order logic evaluator for me. kthxbai 01:15:10 ... 01:15:27 I haven't seen one yet. Should be easy. 01:16:43 Assuming all your types are finite sets. 01:17:07 Otherwise termination is going to be a problem. 01:18:31 If it always terminated, it wouldn't be Turing-complete. 01:18:55 The problem is that a forall on an infinite set would _never_ terminate. 01:19:02 ....so? 01:19:19 a while True loop will never terminate either. 01:19:26 If true. Or an exists, if false. 01:19:56 oerjan: that's where proving comes in. 01:20:20 It doesn't take many brains to tell whether "all natural numbers are natural numbers" is true or false. 01:20:22 I see. And then we are getting into undecidability. 01:20:28 Yep. 01:20:53 'Course, you will have to settle for undecidability in some cases. Nontermination would be fine then, eh? 01:21:46 Writing an evaluator that searches for proofs is "easy". Having it use a reasonable amount of time is hard. 01:25:41 Yeah. 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 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:02:18 Oou really? 06:04:51 Yup :( 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 # 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 Ok, maybe it works better when sung. 11:48:16 argh I have a pun stuck in my head 12:44:13 -!- GregorR_ has joined. 12:44:43 GregorR, GregorR_: ooh, twice the fun! 12:44:47 -!- GregorR has quit (Read error: 104 (Connection reset by peer)). 12:44:59 Sigh 12:45:00 * SimonRC goes 12:52:29 GregorR_, i proved to myself at school you can't do pretty much anything with it 12:53:49 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 oklopol: Oh, you can store and retrieve data. 16:30:29 I've written `cat` 16:30:36 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 16:45:35 sebbu: ???? 16:46:52 /ame 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:22:14 hola 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.