Buffer overflows would've been solved by the haskell implementation. Assuming each of their C translations are free of overflows, the whole thing should be overflow free.
Do you know what "formal" means? It's talking about "formal" as in programs as formal systems, a branch of logicianship that allows you to reason about computation. I would much rather use a completely untested, but entirely formally proven operating environment than a long-lived unproven one. We just haven't gotten to the point where we have proved enough software yet.
Dude, can C's types be reasoned by formal inference? No. Hence, C does not follow typed logical calculus.
C doesn't follow boolean logic either, actually, it just maps to assembly instructions. The best thing you could do to reason about C is to use Dijkstra's proof method which is impractical in a large scale and easy to screw up.
1) L4 is a microkernel. You have no idea what you're talking about. If L4 works, then you could apply similar principles for all the other servers that run in kernel space.
2)This is the largest formal proof ever done in this sort of field. Seriously, the results are not immediately useful, but it's a good start.
Colleges don't disallow Wikipedia because of it's nature, they disallow Wikipedia because it's an encyclopedia -- you can't legitimately source Britannica or any othher encyclopedia in any academic paper, so why should you be allowed to cite Wikipedia?
No, they'll probably have Office Texas 2009, which is like Office 2007, except that it has the XML stuff cut out, and a new language code added: en_TX
Man, that'd be great! Then we'd have things like a helpful paperclip who says, "Y'all need some help with that there letter?" Also, we'll get an official dictionary that only has the useful words like "y'all", "ain't", and "fixins".
I observed the same thing for me, and I am also a pianist.
Also, piano playing means i type with curved fingers unlike some of my fellow comp scientists, and I have never gotten RSI despite typing straight for longer periods than them. Hmm.
Actually, Linus made most of his fortunes from his stock options in Red Hat, given to him by way of thanks, the job at Transmeta was only just getting started then, and his LF work hadn't even begun.
He uses the term "fork" to apply to all the variations of the Linux kernel that exist throughout the distributed git kernel repositories, e.g ACox's fork or Ogawa's fork.
Nah, if they want a standards compliant browser, they'll just code up something around Webkit like Apple and Google have.
The reason they're holding on with IE is they don't want to make a standards compliant browser - it suits them if everyone is locked into using windows for their apps and web apps run bad.
I am an Obama supporter that actually knew what "Change" he wanted, and was quite happy about it too! you might not agree with me, but don't assume all obama supporters blindly supported him without checking the facts
Slashdot Mirror
Buffer overflows would've been solved by the haskell implementation. Assuming each of their C translations are free of overflows, the whole thing should be overflow free.
Do you know what "formal" means? It's talking about "formal" as in programs as formal systems, a branch of logicianship that allows you to reason about computation. I would much rather use a completely untested, but entirely formally proven operating environment than a long-lived unproven one. We just haven't gotten to the point where we have proved enough software yet.
Dude, can C's types be reasoned by formal inference? No. Hence, C does not follow typed logical calculus.
C doesn't follow boolean logic either, actually, it just maps to assembly instructions. The best thing you could do to reason about C is to use Dijkstra's proof method which is impractical in a large scale and easy to screw up.
no, Main is IO. putStrLn does not tell you if it was successful by returning a boolean.
1) L4 is a microkernel. You have no idea what you're talking about. If L4 works, then you could apply similar principles for all the other servers that run in kernel space.
2)This is the largest formal proof ever done in this sort of field. Seriously, the results are not immediately useful, but it's a good start.
Disclaimer: I have worked at NICTA in the past.
Colleges don't disallow Wikipedia because of it's nature, they disallow Wikipedia because it's an encyclopedia -- you can't legitimately source Britannica or any othher encyclopedia in any academic paper, so why should you be allowed to cite Wikipedia?
No, they'll probably have Office Texas 2009, which is like Office 2007, except that it has the XML stuff cut out, and a new language code added: en_TX
Man, that'd be great! Then we'd have things like a helpful paperclip who says, "Y'all need some help with that there letter?" Also, we'll get an official dictionary that only has the useful words like "y'all", "ain't", and "fixins".
(disclaimer: I live in Texas)
FTFY
I observed the same thing for me, and I am also a pianist.
Also, piano playing means i type with curved fingers unlike some of my fellow comp scientists, and I have never gotten RSI despite typing straight for longer periods than them. Hmm.
(ever try comparing Firefox and Seamonkey these days? Guess which is heavier...) .
Oooh, i know! I know! It's Firefox, right?
Do I win something?
As a person that uses google docs, gmail, facebook and slashdot often, I love the fast JS in Chrome.
TraceMonkey isn't nearly as good - it has a strange habit of slowing FF down to a crawl at random intervals.
Yes, in other words, they share much of the same underlying code, but the interface is different.
Opera might not use less memory than Firefox at first, but give Firefox a day to start consuming your RAM and then we'll see.
Well, IE8 still has a horribly incompatible JS and DOM implementation, for starters.
I'm sorry, but IE8 is not really "standards compliant" at all. Fails most of the tests as well.
Actually, Linus made most of his fortunes from his stock options in Red Hat, given to him by way of thanks, the job at Transmeta was only just getting started then, and his LF work hadn't even begun.
Linus thinks differently.
He uses the term "fork" to apply to all the variations of the Linux kernel that exist throughout the distributed git kernel repositories, e.g ACox's fork or Ogawa's fork.
Actually, IE8's JS seems just as garbagey as IE7 -- jQuery et al hide that though.
Nah, if they want a standards compliant browser, they'll just code up something around Webkit like Apple and Google have.
The reason they're holding on with IE is they don't want to make a standards compliant browser - it suits them if everyone is locked into using windows for their apps and web apps run bad.
Alot of tabs and windows in Chromium, which is less memory efficient than Firefox usually, is less ram than that. Way less.
It's the v8 engine. If you use Nitro or something instead, your JS is slower but it works on all platforms - Android does this.
I am an Obama supporter that actually knew what "Change" he wanted, and was quite happy about it too! you might not agree with me, but don't assume all obama supporters blindly supported him without checking the facts
Good luck actually *using* it though.
No, but you wanted to port a perfectly good Linux distribution for mobiles to Minix or L4.
Minix? hah! Architecturally clever, practically useless.
L4 is nice though.
Sure, but in a larger-scale unix system, you'd be suprised how much of it is sh scripts, and other things that depend on it like perl.
It doesn't automatically trim it's content in Leopard for your architecture anyway? Eeugh.