00:34:54 -!- GregorR-L has quit ("Leaving"). 00:43:58 -!- sebbu2 has quit ("@+"). 02:21:21 -!- c|p has quit ("Leaving"). 02:23:16 -!- RodgerTheGreat has quit. 02:25:47 -!- RodgerTheGreat has joined. 02:45:26 i got asked if i had kids today 02:45:30 it was funny 02:46:00 what was the context of this 02:46:23 i was riding my bike past a part and a little kid asks 02:46:33 *park 02:49:33 hunh 02:50:09 that is a unusual question, but as Bill Cosby would say, "Kids say the darnedest things!" 02:51:57 yeah 04:02:52 -!- erider has quit ("I don't sleep because sleep is the cousin of death!"). 06:42:39 -!- oerjan has joined. 07:14:07 -!- GreaseMonkey has joined. 07:32:35 -!- Sgeo has quit (Remote closed the connection). 07:59:59 -!- clog has quit (ended). 08:00:00 -!- clog has joined. 08:30:34 -!- sebbu has joined. 09:49:16 -!- sebbu2 has joined. 10:00:48 -!- oerjan has quit ("leaving"). 10:14:41 -!- jix has joined. 10:16:11 ok, gonna get off now, gnight everyone 10:16:24 -!- sebbu has quit (Read error: 110 (Connection timed out)). 10:16:33 -!- GreaseMonkey has quit ("Hasta la Vista(R)"). 10:29:51 -!- jix has quit ("CommandQ"). 10:37:07 -!- jix has joined. 15:17:33 -!- jix has quit ("CommandQ"). 16:26:58 I wonder if Mel of /The Story of Mel/ is still around 16:28:55 if not, there are probably still some Real Programmers carrying on his proud tradition 16:33:16 there's not even any real computers around anymore 16:37:17 not except when people build their own, anyway 16:37:28 and not in the "order from newegg" sense 16:37:35 out of relays 16:37:57 what most people do is "assembling" computers, not building them 16:41:48 * oklopol goes beep 16:41:52 for no reason 16:42:33 fair enough 16:58:15 -!- c|p has joined. 17:02:54 -!- oerjan has joined. 17:07:37 @who 17:07:42 whoops 17:07:45 wrong window 17:09:37 a likely story 17:09:40 Mel is known to be "Mell Kaye" 17:09:54 @who? isn't that moo or something? 17:11:44 -!- bsmnt_bot has joined. 17:11:58 it's not one of lambdabot's though lambdabot does take some @-commands 17:12:34 i vaguely recall moo commands began with @, like @create 17:13:37 incidentally i am pretty sure there was a lambdamoo 17:13:43 heh 17:14:26 Ah yes, from wikipedia: It is the oldest and most active MOO today, with just under 3000 regular members. 17:15:04 -!- RodgerTheGreat has changed nick to PocketUniverse. 17:15:07 no, lambdabot is to be found on #haskell, among other places 17:15:36 -!- PocketUniverse has changed nick to RodgerTheGreat. 17:16:05 i know what lambdabot is too 17:17:13 it has esoteric languages too, brainfuck and i think unlambda 17:17:57 maybe we could invite it here... 17:21:25 you'll make bsmnt_bot jealous 17:21:42 hmph, it seems not to work presently, otherwise you can /msg it 17:22:28 i suppose a bot with a functional haskell interpreter _would_ make our bots jealous 17:23:18 you can always fork an interpreter 17:25:03 it has an interesting approach to sandboxing, using Haskell's type system to avoid non-pure expressions 17:26:32 that requires a bit more than just invoking an interpreter directly on the code 17:28:30 (actually it invokes a compiler and a dynamical linker. apparently all modern haskell implementations are compiler-based) 17:29:31 although it does run it in a forked process with ulimits, so the sandboxing is not totally type-based. 17:30:31 (I read about this just the other day, i think it was in the haskell-cafe archive) 18:25:08 -!- cmeme has quit (Remote closed the connection). 18:25:30 -!- cmeme has joined. 18:59:27 -!- jix__ has joined. 19:00:04 the world needs a better S 19:00:11 *OS 19:04:25 with fine grained security and a better scripting language than C 19:10:39 fine grained enough to run arbitrary code without a second thought 19:11:17 that's pretty much the dream 19:12:03 it might be possible to make that kind of security more feasible through the use of "secure" trusted compilers that build code that can be considered foolproof 19:12:24 that's not good enough 19:12:33 the security needs to come from the kernel 19:13:31 if compilation became a core service, (which it should if *all* non-kernel software was compiled on the system before execution) it would make perfect sense for it to be part of the kernel 19:13:50 do away with binary executables and you solve a lot of potential issues before they can start. 19:13:56 when i said arbitrary code, i meant arbitrary machine code 19:14:16 not everyone wants to give away their source 19:14:25 in a non virtualized environment, arbitrary machinecode is inherently insecure. 19:14:55 you could avoid having to distribute source by using intermediary interpreted bytecode, and effectively do the same thing as virtualization 19:15:54 you can execute arbitrary machine code safely 19:16:23 because anything dangerous has to go through the kernel 19:20:41 i think the hard part would be managing the tons of permissions data you need to keep track of in an intelligent way 19:23:16 and the methods programs use to modify it 19:27:44 How about requiring compilers to embed safety proofs into the compiled code? 19:28:02 how can you prove safety? 19:28:02 These would have no run-time penalty, as they would be executed by the loader. 19:28:19 The compiler knows more about the program that is represented in the machine code. 19:29:03 exactly 19:29:08 It could know that there aren't any generalised pointers, just refernces and array iterators, but that is hard to tell from the object code 19:29:52 Since it has access to a more abstract representation of the program (i.e. the source code), it has a good idea of all the safety invariants that hold. 19:31:06 It knows what things are always true, that are much easier to check than discover for object code 19:31:10 A Java compiler could annotate the code to say where on the stack was pointers and where was references. 19:31:15 especially if it is written in a language that actually has support for safety invariants 19:31:28 (then show that there is no generalised pointer arithmatic) 19:31:36 oerjan: e.g. Java 19:31:44 Or just about anything modern 19:32:14 You could also prove things like functions not doing ay IO 19:32:23 *cough* Haskell *cough* 19:32:29 how can you prove something like that? 19:33:23 in Haskell, if it doesn't have an IO return type, and unsafePerformIO never gets near it, the function *does* *no* *IO*. 19:33:49 which as i mentioned was how LambdaBot does part of its sandboxing 19:33:51 that's a pretty good mechanism- I'm going to have to explore that language more. 19:33:53 and how can you prove that given only the machine code? 19:34:02 not easily 19:34:11 bsmntbombdood: in general, you don't 19:34:18 right 19:34:20 that is why the *compiler* creates the proof, and the loader checks it 19:34:22 you must construct the proof simultaneously with the machine code 19:34:23 I did say 19:34:46 how do you verify a proof is what i meant 19:35:35 well, to do file IO, you would have to do an OS call or fiddle with the disk devices directly 19:35:47 http://www.cs.cornell.edu/talc/ 19:35:59 therefore, you can show that you do no OS calls, and do not write to certain memory addresses 19:36:08 i think the right approch is to check the permissions related to a system call whenever that call is used 19:36:18 slow 19:36:38 even with a Synthesis-style OS it would be slow 19:36:54 (It gets only a little bit trickier if you add HoF.) 19:37:22 i don't think it would be much slower 19:38:08 depends on your permissions scheme 19:38:37 when to check would probably depend on how often the code is going to run 19:39:10 if it is going to run many times it would be better to have a once-and-for-all proof 19:39:29 i don't think you can have a proof like that 19:40:34 -!- kushalhada has joined. 19:40:49 -!- kushalhada has left (?). 19:42:13 what part of this do you think is unsolvable? 19:43:02 i have no idea how you would construct a proof that could be verified 19:43:56 a proof by definition is verifiable 19:44:11 otherwise it is not a complete proof 19:45:01 you could analize the machine code at loadtime 19:45:56 that wouldn't work even with simple stuff like adding two numbers to get the syscall number 19:45:58 the machine code comes with the proof bundled, that is what proof-carrying code means 19:46:23 how does the proof work 19:47:21 it is just a proof in a machine readable format, that somehow proves that your code satisfies the system's safety protocol 19:47:40 uh huh 19:47:54 it might be equivalent to digital signing or something 19:48:16 or embedded into the functioning of the executable format somehow 19:49:03 i and have no idea how to construct a proof like that 19:49:18 and i highly doubt it's possible 19:49:49 well there are many people working on machine checkable proofs of program properties. 19:50:32 one of the teams is working on creating a certified compiler for Standard ML. it would be the first "real" language with such a compiler. 19:50:59 you can do it with a trusted compiler, sure 19:52:15 apparently they go through Typed Assembly Language, which is asm annotated with types proving the properties of the program 19:53:03 the Curry-Howard isomorphism which says that types and theorems are basically the same thing is important in much of this kind of work 19:53:35 so in a sense Java's types are a simpler version of the same 19:53:48 bsmntbombdood: but you don't need to trust the compiler. If the compiler can explain why the code is safe, and the OS can check it, then it doesn't matter if the executable is a string of random bytes, it must be safe. 19:54:10 SimonRC: "if" 19:58:09 it's not "if", it's "when", and i believe the answer is "within five years" 19:58:10 -!- sebbu has joined. 19:58:24 although not for an entire operating system i guess 19:58:33 bah, 20 years at least 19:59:00 but if the proof is part of the executable, the compiler only has to do it once, right? <:D 19:59:37 right 19:59:38 I don't think you can construct a proof like that 19:59:41 Although MS's Singularity experiment has almost everything written in "safe C#". 20:00:13 bsmntbombdood: depends on the language you are compiling 20:00:17 checking permissions at runtime allows binarys to ignore security if they want to 20:00:50 how the hell can anyone honestly use [C-derivative] and "safe" in the same sentence without negation operators or other complex syntactic shenanigans? 20:00:51 I mean, a C compiler would have more difficulty than a Haskell compiler in checking safety. 20:01:06 RodgerTheGreat: erm C# is not that bad on that angle 20:01:21 you have to mark all "unsafe" code explicitly 20:01:46 And you can write huge swathes of code with no "unsafe" blocks at all 20:01:58 e.g. most of Singularity 20:02:13 eugh 20:02:28 (BTW, I really suggest that you check out the Singularity video on Channel 9 at MSDN.) 20:02:36 C# is better than Java 20:02:46 In my book, when the wheel sucks, build a new one, don't just superglue on retreads. 20:02:54 by which I mean, I like programming in it better 20:03:25 RodgerTheGreat: they have thrown away almost everything except the colour (i.e. the syntax) 20:03:33 although the syntax does suck a bit 20:03:42 but it's not too bad for an imperative language 20:03:50 I guess 20:04:09 I still feel I could do better (which is not an entirely idle statement) 20:04:58 "You need to be free to point the gun wherever you want, but most of the time you *know* you don't want it anywhere near your foot and the compiler should help you out with that." 20:05:11 heh 20:05:58 well, that saves you from some mistakes, but doesn't do anything about the two most dangerous types of coders: malicious hackers and people with no idea what they're doing. 20:06:03 .NET languages are like those lego people: they claim to be different, bu there is a haunting similarity between them. 20:06:10 lol 20:06:11 RodgerTheGreat: heh 20:06:49 There is only one real functional .NET language, and it is not exactly popular. 20:06:55 F# 20:07:10 I've never heard of F# 20:07:36 it is much based on Ocaml, i hear 20:11:52 yes] 20:11:59 doesn't look too bad to me 20:12:24 Although ISTR it has the dreadful syntax for types that OCaml has. 20:13:11 I really don't know how I can hate it so much. 20:13:59 Ocaml is not known for having a pretty default syntax, unlike Haskell 20:14:22 At least it allows the C# syntax for types. 20:14:39 but really, *postfix* type constructors 20:14:43 i understand F# has an alternative syntax 20:14:51 that is inheritance from ML 20:15:27 And an infix type operator (tuple) that neither left nor right associates, but does magic instead, with parentheses being significant? 20:15:39 -!- calamari has joined. 20:15:44 that is also from ML i think 20:16:08 yes, I know 20:16:16 I hate ML's type syntax 20:16:53 And then there's the need for explicit indication of recursion in "let"s. 20:16:58 hey, calamari 20:17:13 there's an idea I wanted to mention to you a few days ago- 20:17:18 -!- sebbu2 has quit (Read error: 110 (Connection timed out)). 20:17:22 FFS people, it is a *functional* language! The compiler should be worrying about that, not the programmer. 20:17:27 * SimonRC stops ranting 20:17:31 hi RodgerTheGreat 20:17:36 shoot 20:17:59 actually without rec you can use the old definition on the right side 20:18:05 like with scheme 20:18:10 yuk 20:18:14 we were discussing how the use of peek, poke and varptr effectively give BASIC pointers- do you think it would be possible to incorporate this type of functionality into BFBASIC? 20:18:59 shouldn't be too hard 20:18:59 obviously, you couldn't use it for accessing arbitrary memory, but you could try to have the compiler map peeks and pokes within memory "owned" by a program 20:19:18 right 20:19:31 it _might_ be possible to access arbitrary memory if you have a fixed memory layout 20:19:46 er, 20:20:00 i guess that's what you meant 20:20:09 oerjan: I don't think he's referring to interpreter bugs 20:20:17 lol 20:20:23 not outside the program 20:20:26 right 20:20:31 I understood exactly what you meant 20:20:48 excellent- we're on the same wavelength 20:20:57 but then with protected memory you couldn't do that anyway 20:21:29 a DIM statement is very similar to a memory allocation in lower-level languages 20:23:41 RodgerTheGreat: here is my suggestion for this... 20:24:02 there is a function called arrows that translates @vars into >>> <<<'s 20:24:12 ok 20:24:14 for example @myvar might be location 123 20:24:38 you could change that function so that it would treat something like @234 specially 20:24:53 so, you're suggesting extending that function to handle peek's "dereferences"? 20:24:59 ah 20:25:01 hm 20:25:01 then @567 in the code would go to memory location 567 20:25:36 then you can use that to write your peek and poke routines 20:26:25 that could work. Now that I'm thinking of this in terms of translation into BF, though, I forsee this could generate some really nasty compiled code 20:26:31 I don't remember what varptr is.. looking that up 20:26:41 well, yeah 20:26:43 varptr returns the memory address of a given variable 20:26:48 but that's the case anyways .. hehe 20:26:53 oh 20:27:00 that should be easy to implement as well 20:27:11 it's how you access a variable via peek and poke so you don't have to just guess wildly. :) 20:27:18 makes sense 20:27:29 do you have the source code to bfbasic ? 20:27:34 I think so 20:27:39 it is available via cvs 20:27:42 okay great 20:27:45 * RodgerTheGreat rifles through his drive 20:28:01 I think the lastest is 1.50 rc 2 20:28:05 latest 20:28:06 effectively, if we compare BASIC to C, varptr() 20:28:09 erk 20:28:24 varptr(x) is equivalent to &x 20:28:36 I would start off by understanding the arrows() function 20:28:41 peek(x) is equivalent to *x 20:29:02 =*x 20:29:22 poke is *x= 20:29:22 and poke x,a is equivalent to *x=a 20:29:26 yeah 20:29:47 anyhow.. if you have any questions about the source code, let me know 20:30:02 ah, I found arrows 20:30:07 if you don't have the cvs version I can dig it up for you 20:30:11 I'll play around with this for a while 20:30:16 okay :) 20:30:25 I have v1.30 20:31:26 that's old 20:31:34 oh. 20:32:24 well, that's the version you have in a .ZIP on your site- that's probably where I got it. 20:32:36 RodgerTheGreat: http://sourceforge.net/cvs/?group_id=59653 20:34:06 oh, dang- you're at 1.41 20:34:34 actually, src contains the latest 20:34:37 1.50rc2 20:35:16 src/ I mean 20:35:30 afk.. 20:35:39 alright, got it 20:35:50 what's new since 1.3? 20:37:14 woah, select case? 20:37:34 I didn't implement that :) 20:38:34 and I must say that AlgebraicExpression.java frightens me a bit 20:39:10 wow, it all makes sense now: http://freefall.purrsia.com/ff200/fv00125.htm 20:39:31 lol 20:39:43 everyone loves a calvin and hobbes reference 20:43:07 * SimonRC reads about the significant parentheses in F# 20:43:18 dear god please make it stop 20:43:58 the type "int -> int" is not the same as "(int -> int)" 20:44:28 wow 20:45:28 neither is "type c = C of int * int" the same as "type c = C of (int * int)", though that was got from ML 20:45:41 * oerjan wonders what SimonRC thinks about python's relation syntax 20:49:29 what's that like? 20:50:32 basically, 1 <= x < y < 3 means the same as in mathematics 20:50:51 ah yes 20:50:58 Perl6 is gonna have that too 20:51:15 That is not *too* bad 20:52:02 Perl 6 is also going to have the amazing | and & operators, which allow things like "a&b=c|d", meaning "(a=c||a=d)&&(b=c||b=d)". 20:52:15 but they have some reasonably clean semantics behind that 20:52:26 that's pretty ugly 20:52:52 it's Perl 20:53:01 or possibly it means "(a=c&&b=c)||(a=d&&b=d)". I forget 20:53:35 is & and | not bitwise and and or? 20:54:01 icon has | like that doesn't it 20:54:23 icon does it in a good way, similar to the List monad in Haskell. 20:54:31 bsmntbombdood: not in Perl 6 20:54:48 bitwise ones have ? prepended 20:55:27 so Perl 6 will not be backwards compatible? 20:55:27 or is that numeric ones? In which case the bitwise ones have + before them, and the character ones I forget about 20:55:31 nope 20:55:46 some very simple things will stay 20:56:19 numeric? 21:00:22 huh? 21:00:54 how is numeric &| different from bitwise? 21:01:18 ints versus strings 21:01:19 dunno 21:10:09 -!- calamari has quit ("Leaving"). 21:41:18 -!- jix__ has quit ("CommandQ"). 22:30:39 -!- ihope has joined. 23:32:10 -!- sebbu has quit ("@+"). 23:54:17 -!- davidmc has joined. 23:55:57 -!- davidmc has changed nick to xTarget.