←2007-06-09 2007-06-10 2007-06-11→ ↑2007 ↑all
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 <bsmntbombdood> i got asked if i had kids today
02:45:30 <bsmntbombdood> it was funny
02:46:00 <RodgerTheGreat> what was the context of this
02:46:23 <bsmntbombdood> i was riding my bike past a part and a little kid asks
02:46:33 <bsmntbombdood> *park
02:49:33 <RodgerTheGreat> hunh
02:50:09 <RodgerTheGreat> that is a unusual question, but as Bill Cosby would say, "Kids say the darnedest things!"
02:51:57 <bsmntbombdood> 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 <GreaseMonkey> 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 <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:17 <RodgerTheGreat> not except when people build their own, anyway
16:37:28 <RodgerTheGreat> and not in the "order from newegg" sense
16:37:35 <bsmntbombdood> out of relays
16:37:57 <RodgerTheGreat> what most people do is "assembling" computers, not building them
16:41:48 * oklopol goes beep
16:41:52 <oklopol> for no reason
16:42:33 <RodgerTheGreat> fair enough
16:58:15 -!- c|p has joined.
17:02:54 -!- oerjan has joined.
17:07:37 <RodgerTheGreat> @who
17:07:42 <RodgerTheGreat> whoops
17:07:45 <RodgerTheGreat> wrong window
17:09:37 <bsmntbombdood> a likely story
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:13:43 <SimonRC> heh
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:25 <bsmntbombdood> you'll make bsmnt_bot jealous
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:23:18 <bsmntbombdood> you can always fork an interpreter
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:00:04 <bsmntbombdood> the world needs a better S
19:00:11 <bsmntbombdood> *OS
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:11:17 <RodgerTheGreat> that's pretty much the dream
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:12:24 <bsmntbombdood> that's not good enough
19:12:33 <bsmntbombdood> the security needs to come from the kernel
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:16 <bsmntbombdood> not everyone wants to give away their source
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:15:54 <bsmntbombdood> you can execute arbitrary machine code safely
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:23:16 <bsmntbombdood> and the methods programs use to modify it
19:27:44 <SimonRC> How about requiring compilers to embed safety proofs into the compiled code?
19:28:02 <bsmntbombdood> how can you prove safety?
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:03 <RodgerTheGreat> exactly
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:36 <SimonRC> oerjan: e.g. Java
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:32:23 <SimonRC> *cough* Haskell *cough*
19:32:29 <bsmntbombdood> how can you prove something like that?
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:02 <SimonRC> not easily
19:34:11 <RodgerTheGreat> bsmntbombdood: in general, you don't
19:34:18 <bsmntbombdood> right
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:34:23 <SimonRC> I did say
19:34:46 <bsmntbombdood> how do you verify a proof is what i meant
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:18 <SimonRC> slow
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:37:22 <bsmntbombdood> i don't think it would be much slower
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:39:29 <bsmntbombdood> 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 <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:01 <bsmntbombdood> you could analize the machine code at loadtime
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:46:23 <bsmntbombdood> how does the proof work
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:40 <bsmntbombdood> uh huh
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:18 <bsmntbombdood> and i highly doubt it's possible
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:50:59 <bsmntbombdood> you can do it with a trusted compiler, sure
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:54:10 <bsmntbombdood> SimonRC: "if"
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:58:33 <SimonRC> bah, 20 years at least
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:37 <oerjan> right
19:59:38 <bsmntbombdood> I don't think you can construct a proof like that
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:01:58 <SimonRC> e.g. most of Singularity
20:02:13 <RodgerTheGreat> eugh
20:02:28 <SimonRC> (BTW, I really suggest that you check out the Singularity video on Channel 9 at MSDN.)
20:02:36 <SimonRC> C# is better than Java
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:03:50 <RodgerTheGreat> I guess
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:11 <RodgerTheGreat> heh
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:10 <RodgerTheGreat> lol
20:06:11 <SimonRC> RodgerTheGreat: heh
20:06:49 <SimonRC> There is only one real functional .NET language, and it is not exactly popular.
20:06:55 <SimonRC> F#
20:07:10 <RodgerTheGreat> I've never heard of F#
20:07:36 <oerjan> it is much based on Ocaml, i hear
20:11:52 <SimonRC> yes]
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:08 <SimonRC> yes, I know
20:16:16 <SimonRC> I hate ML's type syntax
20:16:53 <SimonRC> And then there's the need for explicit indication of recursion in "let"s.
20:16:58 <RodgerTheGreat> hey, calamari
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:27 * SimonRC stops ranting
20:17:31 <calamari> hi RodgerTheGreat
20:17:36 <calamari> shoot
20:17:59 <oerjan> actually without rec you can use the old definition on the right side
20:18:05 <oerjan> like with scheme
20:18:10 <SimonRC> yuk
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 <calamari> shouldn't be too hard
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:18 <calamari> right
20:19:31 <oerjan> it _might_ be possible to access arbitrary memory if you have a fixed memory layout
20:19:46 <oerjan> er,
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:17 <RodgerTheGreat> lol
20:20:23 <oerjan> not outside the program
20:20:26 <calamari> right
20:20:31 <calamari> I understood exactly what you meant
20:20:48 <RodgerTheGreat> excellent- we're on the same wavelength
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:12 <RodgerTheGreat> ok
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:24:59 <RodgerTheGreat> ah
20:25:01 <RodgerTheGreat> hm
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:41 <calamari> well, yeah
20:26:43 <RodgerTheGreat> varptr returns the memory address of a given variable
20:26:48 <calamari> but that's the case anyways .. hehe
20:26:53 <calamari> oh
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:18 <calamari> makes sense
20:27:29 <calamari> do you have the source code to bfbasic ?
20:27:34 <RodgerTheGreat> I think so
20:27:39 <calamari> it is available via cvs
20:27:42 <calamari> okay great
20:27:45 * RodgerTheGreat rifles through his drive
20:28:01 <calamari> I think the lastest is 1.50 rc 2
20:28:05 <calamari> latest
20:28:06 <RodgerTheGreat> effectively, if we compare BASIC to C, varptr()
20:28:09 <RodgerTheGreat> erk
20:28:24 <RodgerTheGreat> varptr(x) is equivalent to &x
20:28:36 <calamari> I would start off by understanding the arrows() function
20:28:41 <RodgerTheGreat> peek(x) is equivalent to *x
20:29:02 <calamari> =*x
20:29:22 <calamari> poke is *x=
20:29:22 <RodgerTheGreat> and poke x,a is equivalent to *x=a
20:29:26 <RodgerTheGreat> yeah
20:29:47 <calamari> anyhow.. if you have any questions about the source code, let me know
20:30:02 <RodgerTheGreat> ah, I found arrows
20:30:07 <calamari> if you don't have the cvs version I can dig it up for you
20:30:11 <RodgerTheGreat> I'll play around with this for a while
20:30:16 <calamari> okay :)
20:30:25 <RodgerTheGreat> I have v1.30
20:31:26 <calamari> that's old
20:31:34 <RodgerTheGreat> oh.
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:06 <RodgerTheGreat> oh, dang- you're at 1.41
20:34:34 <calamari> actually, src contains the latest
20:34:37 <calamari> 1.50rc2
20:35:16 <calamari> src/ I mean
20:35:30 <calamari> afk..
20:35:39 <RodgerTheGreat> alright, got it
20:35:50 <RodgerTheGreat> what's new since 1.3?
20:37:14 <RodgerTheGreat> woah, select case?
20:37:34 <calamari> I didn't implement that :)
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:39:31 <RodgerTheGreat> lol
20:39:43 <RodgerTheGreat> everyone loves a calvin and hobbes reference
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:44:28 <oerjan> wow
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:49:29 <SimonRC> what's that like?
20:50:32 <oerjan> basically, 1 <= x < y < 3 means the same as in mathematics
20:50:51 <SimonRC> ah yes
20:50:58 <SimonRC> Perl6 is gonna have that too
20:51:15 <SimonRC> That is not *too* bad
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:52:26 <bsmntbombdood> that's pretty ugly
20:52:52 <SimonRC> it's Perl
20:53:01 <SimonRC> or possibly it means "(a=c&&b=c)||(a=d&&b=d)". I forget
20:53:35 <bsmntbombdood> is & and | not bitwise and and or?
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:31 <SimonRC> nope
20:55:46 <SimonRC> some very simple things will stay
20:56:19 <oerjan> numeric?
21:00:22 <SimonRC> huh?
21:00:54 <oerjan> how is numeric &| different from bitwise?
21:01:18 <bsmntbombdood> ints versus strings
21:01:19 <SimonRC> 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.
←2007-06-09 2007-06-10 2007-06-11→ ↑2007 ↑all