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:46:23 <bsmntbombdood> i was riding my bike past a part and a little kid asks
02:50:09 <RodgerTheGreat> that is a unusual question, but as Bill Cosby would say, "Kids say the darnedest things!"
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: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 <bsmntbombdood> I wonder if Mel of /The Story of Mel/ is still around
16:28:55 <RodgerTheGreat> if not, there are probably still some Real Programmers carrying on his proud tradition
16:33:16 <bsmntbombdood> there's not even any real computers around anymore
16:37:57 <RodgerTheGreat> what most people do is "assembling" computers, not building them
16:58:15 -!- c|p has joined.
17:02:54 -!- oerjan has joined.
17:09:40 <SimonRC> Mel is known to be "Mell Kaye"
17:09:54 <oerjan> @who? isn't that moo or something?
17:11:44 -!- bsmnt_bot has joined.
17:11:58 <SimonRC> it's not one of lambdabot's though lambdabot does take some @-commands
17:12:34 <oerjan> i vaguely recall moo commands began with @, like @create
17:13:37 <oerjan> incidentally i am pretty sure there was a lambdamoo
17:14:26 <oerjan> 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 <SimonRC> no, lambdabot is to be found on #haskell, among other places
17:15:36 -!- PocketUniverse has changed nick to RodgerTheGreat.
17:16:05 <oerjan> i know what lambdabot is too
17:17:13 <oerjan> it has esoteric languages too, brainfuck and i think unlambda
17:17:57 <oerjan> maybe we could invite it here...
17:21:42 <oerjan> hmph, it seems not to work presently, otherwise you can /msg it
17:22:28 <oerjan> i suppose a bot with a functional haskell interpreter _would_ make our bots jealous
17:25:03 <oerjan> it has an interesting approach to sandboxing, using Haskell's type system to avoid non-pure expressions
17:26:32 <oerjan> that requires a bit more than just invoking an interpreter directly on the code
17:28:30 <oerjan> (actually it invokes a compiler and a dynamical linker. apparently all modern haskell implementations are compiler-based)
17:29:31 <oerjan> although it does run it in a forked process with ulimits, so the sandboxing is not totally type-based.
17:30:31 <oerjan> (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:04:25 <bsmntbombdood> with fine grained security and a better scripting language than C
19:10:39 <bsmntbombdood> fine grained enough to run arbitrary code without a second thought
19:12:03 <RodgerTheGreat> 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:13:31 <RodgerTheGreat> 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 <RodgerTheGreat> do away with binary executables and you solve a lot of potential issues before they can start.
19:13:56 <bsmntbombdood> when i said arbitrary code, i meant arbitrary machine code
19:14:25 <RodgerTheGreat> in a non virtualized environment, arbitrary machinecode is inherently insecure.
19:14:55 <RodgerTheGreat> you could avoid having to distribute source by using intermediary interpreted bytecode, and effectively do the same thing as virtualization
19:16:23 <bsmntbombdood> because anything dangerous has to go through the kernel
19:20:41 <bsmntbombdood> i think the hard part would be managing the tons of permissions data you need to keep track of in an intelligent way
19:27:44 <SimonRC> How about requiring compilers to embed safety proofs into the compiled code?
19:28:02 <SimonRC> These would have no run-time penalty, as they would be executed by the loader.
19:28:19 <SimonRC> The compiler knows more about the program that is represented in the machine code.
19:29:08 <SimonRC> 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 <SimonRC> 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 <SimonRC> It knows what things are always true, that are much easier to check than discover for object code
19:31:10 <SimonRC> A Java compiler could annotate the code to say where on the stack was pointers and where was references.
19:31:15 <oerjan> especially if it is written in a language that actually has support for safety invariants
19:31:28 <SimonRC> (then show that there is no generalised pointer arithmatic)
19:31:44 <SimonRC> Or just about anything modern
19:32:14 <SimonRC> You could also prove things like functions not doing ay IO
19:33:23 <SimonRC> 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 <oerjan> which as i mentioned was how LambdaBot does part of its sandboxing
19:33:51 <RodgerTheGreat> that's a pretty good mechanism- I'm going to have to explore that language more.
19:33:53 <bsmntbombdood> and how can you prove that given only the machine code?
19:34:20 <SimonRC> that is why the *compiler* creates the proof, and the loader checks it
19:34:22 <oerjan> you must construct the proof simultaneously with the machine code
19:35:35 <SimonRC> well, to do file IO, you would have to do an OS call or fiddle with the disk devices directly
19:35:47 <oerjan> http://www.cs.cornell.edu/talc/
19:35:59 <SimonRC> therefore, you can show that you do no OS calls, and do not write to certain memory addresses
19:36:08 <bsmntbombdood> i think the right approch is to check the permissions related to a system call whenever that call is used
19:36:38 <SimonRC> even with a Synthesis-style OS it would be slow
19:36:54 <SimonRC> (It gets only a little bit trickier if you add HoF.)
19:38:08 <SimonRC> depends on your permissions scheme
19:38:37 <oerjan> when to check would probably depend on how often the code is going to run
19:39:10 <oerjan> if it is going to run many times it would be better to have a once-and-for-all proof
19:40:34 -!- kushalhada has joined.
19:40:49 -!- kushalhada has left (?).
19:42:13 <oerjan> what part of this do you think is unsolvable?
19:43:02 <bsmntbombdood> i have no idea how you would construct a proof that could be verified
19:43:56 <oerjan> a proof by definition is verifiable
19:44:11 <oerjan> otherwise it is not a complete proof
19:45:56 <bsmntbombdood> that wouldn't work even with simple stuff like adding two numbers to get the syscall number
19:45:58 <oerjan> the machine code comes with the proof bundled, that is what proof-carrying code means
19:47:21 <oerjan> it is just a proof in a machine readable format, that somehow proves that your code satisfies the system's safety protocol
19:47:54 <RodgerTheGreat> it might be equivalent to digital signing or something
19:48:16 <RodgerTheGreat> or embedded into the functioning of the executable format somehow
19:49:03 <bsmntbombdood> i and have no idea how to construct a proof like that
19:49:49 <oerjan> well there are many people working on machine checkable proofs of program properties.
19:50:32 <oerjan> 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:52:15 <oerjan> apparently they go through Typed Assembly Language, which is asm annotated with types proving the properties of the program
19:53:03 <oerjan> 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 <oerjan> so in a sense Java's types are a simpler version of the same
19:53:48 <SimonRC> 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:58:09 <oerjan> 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 <oerjan> although not for an entire operating system i guess
19:59:00 <RodgerTheGreat> but if the proof is part of the executable, the compiler only has to do it once, right? <:D
19:59:41 <SimonRC> Although MS's Singularity experiment has almost everything written in "safe C#".
20:00:13 <SimonRC> bsmntbombdood: depends on the language you are compiling
20:00:17 <bsmntbombdood> checking permissions at runtime allows binarys to ignore security if they want to
20:00:50 <RodgerTheGreat> 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 <SimonRC> I mean, a C compiler would have more difficulty than a Haskell compiler in checking safety.
20:01:06 <SimonRC> RodgerTheGreat: erm C# is not that bad on that angle
20:01:21 <SimonRC> you have to mark all "unsafe" code explicitly
20:01:46 <SimonRC> And you can write huge swathes of code with no "unsafe" blocks at all
20:02:28 <SimonRC> (BTW, I really suggest that you check out the Singularity video on Channel 9 at MSDN.)
20:02:46 <RodgerTheGreat> In my book, when the wheel sucks, build a new one, don't just superglue on retreads.
20:02:54 <SimonRC> by which I mean, I like programming in it better
20:03:25 <SimonRC> RodgerTheGreat: they have thrown away almost everything except the colour (i.e. the syntax)
20:03:33 <SimonRC> although the syntax does suck a bit
20:03:42 <SimonRC> but it's not too bad for an imperative language
20:04:09 <RodgerTheGreat> I still feel I could do better (which is not an entirely idle statement)
20:04:58 <SimonRC> "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:58 <RodgerTheGreat> 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 <SimonRC> .NET languages are like those lego people: they claim to be different, bu there is a haunting similarity between them.
20:06:49 <SimonRC> There is only one real functional .NET language, and it is not exactly popular.
20:07:36 <oerjan> it is much based on Ocaml, i hear
20:11:59 <SimonRC> doesn't look too bad to me
20:12:24 <SimonRC> Although ISTR it has the dreadful syntax for types that OCaml has.
20:13:11 <SimonRC> I really don't know how I can hate it so much.
20:13:59 <oerjan> Ocaml is not known for having a pretty default syntax, unlike Haskell
20:14:22 <SimonRC> At least it allows the C# syntax for types.
20:14:39 <SimonRC> but really, *postfix* type constructors
20:14:43 <oerjan> i understand F# has an alternative syntax
20:14:51 <oerjan> that is inheritance from ML
20:15:27 <SimonRC> 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 <oerjan> that is also from ML i think
20:16:53 <SimonRC> And then there's the need for explicit indication of recursion in "let"s.
20:17:13 <RodgerTheGreat> 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 <SimonRC> FFS people, it is a *functional* language! The compiler should be worrying about that, not the programmer.
20:17:59 <oerjan> actually without rec you can use the old definition on the right side
20:18:14 <RodgerTheGreat> 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 <RodgerTheGreat> 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:31 <oerjan> it _might_ be possible to access arbitrary memory if you have a fixed memory layout
20:20:00 <oerjan> i guess that's what you meant
20:20:09 <calamari> oerjan: I don't think he's referring to interpreter bugs
20:20:23 <oerjan> not outside the program
20:20:31 <calamari> I understood exactly what you meant
20:20:57 <oerjan> but then with protected memory you couldn't do that anyway
20:21:29 <RodgerTheGreat> a DIM statement is very similar to a memory allocation in lower-level languages
20:23:41 <calamari> RodgerTheGreat: here is my suggestion for this...
20:24:02 <calamari> there is a function called arrows that translates @vars into >>> <<<'s
20:24:14 <calamari> for example @myvar might be location 123
20:24:38 <calamari> you could change that function so that it would treat something like @234 specially
20:24:53 <RodgerTheGreat> so, you're suggesting extending that function to handle peek's "dereferences"?
20:25:01 <calamari> then @567 in the code would go to memory location 567
20:25:36 <calamari> then you can use that to write your peek and poke routines
20:26:25 <RodgerTheGreat> 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 <calamari> I don't remember what varptr is.. looking that up
20:26:48 <calamari> but that's the case anyways .. hehe
20:27:00 <calamari> that should be easy to implement as well
20:27:11 <RodgerTheGreat> it's how you access a variable via peek and poke so you don't have to just guess wildly. :)
20:27:29 <calamari> do you have the source code to bfbasic ?
20:28:01 <calamari> I think the lastest is 1.50 rc 2
20:28:36 <calamari> I would start off by understanding the arrows() function
20:29:47 <calamari> anyhow.. if you have any questions about the source code, let me know
20:30:07 <calamari> if you don't have the cvs version I can dig it up for you
20:32:24 <RodgerTheGreat> well, that's the version you have in a .ZIP on your site- that's probably where I got it.
20:32:36 <calamari> RodgerTheGreat: http://sourceforge.net/cvs/?group_id=59653
20:34:34 <calamari> actually, src contains the latest
20:38:34 <RodgerTheGreat> and I must say that AlgebraicExpression.java frightens me a bit
20:39:10 <oerjan> wow, it all makes sense now: http://freefall.purrsia.com/ff200/fv00125.htm
20:43:07 * SimonRC reads about the significant parentheses in F#
20:43:18 <SimonRC> dear god please make it stop
20:43:58 <SimonRC> the type "int -> int" is not the same as "(int -> int)"
20:45:28 <SimonRC> 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:50:32 <oerjan> basically, 1 <= x < y < 3 means the same as in mathematics
20:50:58 <SimonRC> Perl6 is gonna have that too
20:52:02 <SimonRC> 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 <SimonRC> but they have some reasonably clean semantics behind that
20:53:01 <SimonRC> or possibly it means "(a=c&&b=c)||(a=d&&b=d)". I forget
20:54:01 <oerjan> icon has | like that doesn't it
20:54:23 <SimonRC> icon does it in a good way, similar to the List monad in Haskell.
20:54:31 <SimonRC> bsmntbombdood: not in Perl 6
20:54:48 <SimonRC> bitwise ones have ? prepended
20:55:27 <oerjan> so Perl 6 will not be backwards compatible?
20:55:27 <SimonRC> or is that numeric ones? In which case the bitwise ones have + before them, and the character ones I forget about
20:55:46 <SimonRC> some very simple things will stay
21:00:54 <oerjan> how is numeric &| different from bitwise?
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.