Comment Re:Now all we need.... (Score 1) 517
I work at NICTA from time to time. Will raise this with them.
I work at NICTA from time to time. Will raise this with them.
Haskell's garbage collection works (or should work) based on formal inference -- seeing as they translated the haskell to C manually, they would have proved the garbage collection as part of the deal. Also, haskell's prelude and basic libraries have already been formally proven.
Because of formal inference, a good Haskell compiler knows exactly when and what will be garbage collected at compile time - there is no mark-and-sweep approach like Java. It's no worse that manually freeing stuff in C, in fact it's substantially better.
L4 doesn't delegate memory management to a process, that is impossible, because it would then have to manage memory for the memory management process.
It would only kill the hardware it's dealing with, likely, so the kernel might still keep on chugging. All the kernel needs is memory and cpu after all
Thanks!
Malware would have a much harder time making a root exploit in this case.
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?
1 + 1 = 3, for large values of 1.