Slashdot Mirror

They don't track body position in the C6. They use the C4 for that, and that part of the setup is pretty buggy anyways. This page has a decent runthrough of the projects they do http://www.vrac.iastate.edu/research/index.php. Mostly it's industrial simulations for John Deere, P&G, etc. I worked on one art project there that was kind of neat, but it really suffered from the technology. Hopefully having some better hardware will let them do some more visually engaging stuff, although I sort of doubt it.

They don't track body position in the C6. They use the C4 for that, and that part of the setup is pretty buggy anyways. This page has a decent runthrough of the projects they do http://www.vrac.iastate.edu/research/index.php. Mostly it's industrial simulations for John Deere, P&G, etc. I worked on one art project there that was kind of neat, but it really suffered from the technology. Hopefully having some better hardware will let them do some more visually engaging stuff, although I sort of doubt it.

Former SGI CEO Ed McCracken was a graduate of the ISU College of Engineering. In 1992 he donated $5 million worth of SGI equipment to the university. I'm not sure what (if any) of the original donation went to what became the VRAC, but the widespread use of SGI equipment in the ISU College of Engineering certainly contributed to the use of SGI hardware in the VRAC.

Design by Contract is particularly nice if you are willing to spend a little extra effort to write very reliable code, but it would be even better if there were good theorum provers out there to verify that contracts will always hold and warn if they don't. The would be much more developer friendly than the predicate calculus normally associated with formal methods.

If that's what you're looking for then I would suggest that you take some time to check out JML and ESC/Java2 which provides almost exactly that functionality for Java. It's not as clean as Eiffel as the contracts have be be kludged into Java as add-on annotation in comments, but all the functionality you'd want in a good expressive DbC system is there in JML, and ESC/Java2 provides a static checker/theorem prover that can attempt to verify contracts and provide warn you when they might fail. It also provides a number of other strong static checks based on JML annotations, allowing you to have high degree of confidence in well annotated code that passes ESC/Java2. Honestly, download JML, JMLEclipse and ESC/Java2 and try them out - you'll be amazed the number of subtle errors that can be quickly and efficiently caught!

His belief that a method should never return a value and have a side effect is particularly bad. Writing a stack with get_top() and remove_top() instead of pop() is a little weird.

It seems odd, but it does have nice aspects, particularly if you're used to a more functional perspective: it goes a long way toward isolating side effects and allowing better reasoning about the scope of effects that a given block of code may have. It certainly makes sense to me.

Jedidiah.

I am a Ph.D. student in computer engineering at Iowa State, and our program may be of interest to you. We have several faculty members doing forensics research in areas such as detecting illegal pornography and attack attribution. The department also has a computer forensics lab, and offers a specific course in Computer Forensics that includes projects where drive images are examined using EnCase and FTK in order to locate and recover evidence.

Probably the best advice I can give on selecting any program is checking out the courses that are offered and what the faculty in that department are working on. It may take some time and effort, but can really pay off. An additional benefit with our program at Iowa State is that most of our computer security courses are offered through distance education. So if you are undecided, you can take a course or two and decide if it is something you want to pursue.

I am a Ph.D. student in computer engineering at Iowa State, and our program may be of interest to you. We have several faculty members doing forensics research in areas such as detecting illegal pornography and attack attribution. The department also has a computer forensics lab, and offers a specific course in Computer Forensics that includes projects where drive images are examined using EnCase and FTK in order to locate and recover evidence.

Probably the best advice I can give on selecting any program is checking out the courses that are offered and what the faculty in that department are working on. It may take some time and effort, but can really pay off. An additional benefit with our program at Iowa State is that most of our computer security courses are offered through distance education. So if you are undecided, you can take a course or two and decide if it is something you want to pursue.

I won't need to buy clay pigeons any more!

There are a lot of fields in the security area, some deal with networks, but many do not. You need to spend some time researching what "specialties" there are in the broader field.

For example, computer forensics is a specialty within the security field, and it can mean a lot of things. It could mean examining network logs to trace the source of a DDoS attack, or to determine the full scope of an attack. Ex. We know we were hacked, but did they get access to accounting or our development systems? Determining what was compromised is important and may require days of detailed analysis and little to no programming. Forensics may also mean using tools such as EnCase or Forensic ToolKit (FTK) to examine a captured hard drive for evidence. You may be looking for illegal pornography, stolen data or hidden records. Some of them may be deleted, obfuscated (such as changing a .xls to a .jpg) or hidden in slack space on a drive. Sometimes this can be fairly straightforward, and sometimes it isn't.

A lot of areas in the security field require entirely different skillsets, so having an idea of what you want to do is vital. Using the forensics example, if you want to examine network logs, you need to have a very strong understanding of networking and protocols. If you want to examine hard drives for evidence, you need a strong understanding of file formats and how OSes and hard drives handle data. In general you need a good understanding of the law, especially evidence collection. This knowledge might be helpful if you want to conduct Sarbanes-Oxley (SOX) audits, but not nearly as much as a solid understanding of business principles, and the ability to understand how the internal information is handled and stored. All of these may be handled by the same forensics team, (or one very overworked individual), requiring a lot of knowledge and skills.

With that in mind, I would recommend taking some classes in the security field. The college I'm at (Iowa State University) has a great program in Information Assurance, and has some great core classes for learning about the field. They are available through our Engineering Distance Education group, and the profs take into account that there are off-campus/non-traditional students taking the courses.

Otherwise, my advice is to talk to people in the field and ask them what they do, what their time is spent on and what skills they need to do their job. Take some time to find out what is available before trying to gather the knowledge or the skills - they might not be that helpful in what you ultimately decide to do.

There are a lot of fields in the security area, some deal with networks, but many do not. You need to spend some time researching what "specialties" there are in the broader field.

For example, computer forensics is a specialty within the security field, and it can mean a lot of things. It could mean examining network logs to trace the source of a DDoS attack, or to determine the full scope of an attack. Ex. We know we were hacked, but did they get access to accounting or our development systems? Determining what was compromised is important and may require days of detailed analysis and little to no programming. Forensics may also mean using tools such as EnCase or Forensic ToolKit (FTK) to examine a captured hard drive for evidence. You may be looking for illegal pornography, stolen data or hidden records. Some of them may be deleted, obfuscated (such as changing a .xls to a .jpg) or hidden in slack space on a drive. Sometimes this can be fairly straightforward, and sometimes it isn't.

A lot of areas in the security field require entirely different skillsets, so having an idea of what you want to do is vital. Using the forensics example, if you want to examine network logs, you need to have a very strong understanding of networking and protocols. If you want to examine hard drives for evidence, you need a strong understanding of file formats and how OSes and hard drives handle data. In general you need a good understanding of the law, especially evidence collection. This knowledge might be helpful if you want to conduct Sarbanes-Oxley (SOX) audits, but not nearly as much as a solid understanding of business principles, and the ability to understand how the internal information is handled and stored. All of these may be handled by the same forensics team, (or one very overworked individual), requiring a lot of knowledge and skills.

With that in mind, I would recommend taking some classes in the security field. The college I'm at (Iowa State University) has a great program in Information Assurance, and has some great core classes for learning about the field. They are available through our Engineering Distance Education group, and the profs take into account that there are off-campus/non-traditional students taking the courses.

Otherwise, my advice is to talk to people in the field and ask them what they do, what their time is spent on and what skills they need to do their job. Take some time to find out what is available before trying to gather the knowledge or the skills - they might not be that helpful in what you ultimately decide to do.

Studies have indeed shown a causal relationship between video games and hyperactivity, attention deficit, and violence.

You know, I get really, really tired of people pulling the "studies have shown" card. It would be nice (better than nice, it would decrease the flow of FUD on the internet and IRL) if people were held to the same standards that people publishing scholarly papers were held to; namely, publishing your sources. Watch and learn, kids:

Most studies found a correlation, not a causal relationship, which means the research could simply show that aggressive people like aggressive entertainment.

Yes, I'm drumming the words of Henry Jenkins. But perhaps this will help? Or this? I mean, try these phrases on for size:

Even if we accept that there is a correlation between amount of time spent playing (violent) video games and aggressive behavior, there is no reason to think that games are the cause of aggression.

However, the correlational nature of Study 1 means that causal statements are risky at best. It could be that obtained video game game violence links to aggressive and nonaggressive delinquency are wholly due to the fact that highly aggressive individuals are especially are especially attracted to violent video games.

Now, I could attack your argument (and in a way, at least, I have) but I take issue mostly with the bandying of the phrase "studies have shown" without so much as a reference to the studies in question. It is the worst kind of sloppy intellectualism that presumes all people everywhere are aware of these studies and that their validity is a foregone conclusion; indeed, it smacks of my mother-in-law forwarding her latest round of AOL-Microsoft mergers and get-rich-quick email forwarding scams.

If you are really intersted:

http://www.psychology.iastate.edu/faculty/caa/Vide o_Game_FAQs.html
http://www.medicalnewstoday.com/medicalnews.php?ne wsid=31961
http://www.youngmedia.org.au/mediachildren/05_07_v iolence_anderson.htm

Yup. It is all misleading math.

If you are interested in disproving it, it is relatively simple. Science is an open process. Do your own study. But major studies by disinterested third parties have demonstrated a positive, causal relationship between video games and violence. Other studies have confirmed. Peer review has taken place.

If you simply say "I don't believe it.. politics", I will lump you in with global warming disbelievers, 6,000 year old earth believers who think smoking does not cause cancer.

This does not seem to be the case. I'm not talking here about walking up to a random man on the street and shooting him, but violent video games do seem to increase violent behavior. For example, people who play violent video games and are then given a choice regarding how long to shock somebody, tend to give longer and more intense shocks than people who haven't played video games.

This article has been linked to a lot already, but I don't think more exposure can hurt: Anderson & Bushman, 2001

The reason to fight against the idea of censoring violent video games has nothing to do with whether or not games make you violent. You should fight against the idea of censoring violent video games because it's censorship, and if we value our freedom, then we should abhor it when ideas are censored. Yes, some ideas will make you violent (apparantly, for example, the idea that teleportation research on mars has just transported in demons from hell, but also other, more political ideas) but you should not, in general, suppress anything that may make someone act in violent ways.

The actual scientific study is available from
http://www.psychology.iastate.edu/faculty/caa/abst racts/2000-2004/01AB.pdf

... is a stark raving bozo. Why does he get a respectful hearing, anywhere?

It's just a darn shame they stole all that technology, eh? Although Eckert disputes it at the end of the interview, the court found that: "...John Vincent Atanasoff and Clifford Berry had constructed the first electronic digital computer at Iowa State College in the 1939 - 1942 period. He had also ruled that John Mauchly and J. Presper Eckert, who had for more than twenty-five years been feted, trumpeted, and honored as the co-inventors of the first electronic digital computer, were not entitled to the patent upon which that honor was based. Furthermore, Judge Larson had ruled that Mauchly had pirated Atanasoff's ideas, and for more than thirty years had palmed those ideas off on the world as the product of his own genius." Full Q&A can be found here: http://www.scl.ameslab.gov/ABC/Trial.html Court documents can be found here: http://www.cs.iastate.edu/jva/court-papers/index.s html

And you conclude that from those buggy BNFs you linked to? Or something else?

Ruby:
puts 'Hello World!'

Java (must be in file: "Hello.java"):
public class Hello {
public static void main(String[] args) {
System.out.println("Hello world!");
}
}

Er, hello? I know you were only criticizing the BNF's I cited, but think we can put all this "java is simpler" garbage to rest now.

As mentioned previously, this sort of thing is being/has been done. One project I am familiar with is the Internet-scale Event and Attack Generation Environment (ISEAGE) project at Iowa State University.

Its webpage, has an overview of the project and documentation on its architecture and implementation. I think one of the key aspects of the project can be found in the overview: "Unlike computer-based simulations, real attacks will be played out against real equipment."

ISEAGE is approaching security from a real-world perspective, using real world devices. Sure, your software/hardware might be secure when the attacks are played against it; but is it secure when those attacks when there are dozens of attacks occuring simultaneously? What about when it is being hit by thousands of requests, or is under a DDoS attack? What happens when devices decide to start breaking the protocols, or the rules? What happens if a device physically fails? What is the effect of a device overheating during a DDoS attack? How do you simulate this/test for this other than hooking it up and hammering it with a DDoS attack?

This is the kind of information that is needed to prevent or mitigate an attack, but can't be found by reading code or running a scanner. How did the US figure out how to build rockets? We built some, they blew up, and better ones got built. The real world isn't the same as a lab.

Agriculture is the worst mistake in the history of the human race, quoth Diamond. His opinions are to be taken very lightly.

The computer was patented. Presper Eckert and John Mauchly of the University of Pennsylvania held the patent for awhile based on their work on the ENIAC until a court case ruled that the ENIAC was a derivative of the Atanasoff Berry Computer, invented by John Atanasoff and Clifford Berry at Iowa State University. You can read the court documents if you really want. http://www.cs.iastate.edu/jva/court-papers/

Thanks for a thoughtful post.

And why are softwares so buggy and have such a lousy reputation anyway? Not to start a flamewar, but let's just list a few possible "reaons" here:

I think, to be honest, that it is a combination of a number of the factors you mention.

Why aren't schools teaching this methodoly thoroughly? Why aren't this toolset and programming language taught in school by default?

To do proper formal specification, one of the key parts of Praxis' Correct by Construction approach, does require a decent solid mathematical background. I think a lot of CS departments, facing students who want vocational training, struggle to demand the sort of mathematical requirements that are needed. As to SPARK - it is something that Praxis developed themselves, and it is proprietary (the toolset at least, the annotation language is well documented). You can pick up a book and learn the language, but the tools cost money if you want to use them commercially. On the other hand, the base specification language Praxis uses, Z, is entirely open, and there are a variety of freely available tools for it. There are also other specification langauges (I quite like CASL which has a number of useful extensions) that have freely available tools associated with them. There's also JML and ESC/Java2 which are freely available and seek to provide the same sort of functionality or Java that SPARK adds to Ada. There are places that teach JML, but they are still few and far between.

Programmers are asked to do the impossible.

I think this is a big part of it in some ways. Partly this is because, for a large number of software projects, the degree of exactness and quality just isn't required. I don't need a professional architect to help me build a doghouse in my backyard (though I'd certainly want one if I was building a skyscraper), and I don't need assurances of bug free software for a simple web front-end to a database. At the same time programmers are often unwilling to let customers know exactly what the limits are when developing software. To quote you: "If a customer dares to ask a civil engineer to add 2 more stories between the 3rd and 4th floor after the custom-built building is finished, guess what would the civil engineer say?"; if software engineers aren't prepared to stand up for quality and tell customers that somethings can't be done without sacrificing the quality of the product the problem will remain. In part I think this is due to the fact that software development is a young industry, and programmers are still of the mentality that they need to do everything they possibly can to please a customer. Partly it's because software projects are diverse (as are building projects!) and sometimes it's okay to make late changes; sometimes it's how things ought to be done - the key is to identify exactly what sort of project it is as early as you can. Are you building a treehouse for your kids, which doesn't require exactness and benefits from incremental design and feedback, or are you building a 4 story building where quality is important, and late changes will jepordise that?

Programmers are a bunch of bozos who know shit about proper engineering.

Sadly this is partly the case. There are an awful lot of cowboys out there when it comes to software engineering. There are, of course, a lot of fantastic programmers as well who are otherwise beset by some of the other points mentioned. There is, however, a remarkable degree of tolerance for cowboys, sloppiness and lack of quality in software engineering that you don't see in other engineering disciplines. Partly I thin

Praxis uses SPARK Ada, which is a subset of the Ada programming language and annotations that provide for extended static checking, and theorem proving. You can find more about SPARK at the Praxis website, or the Wikipedia article isn't too bad. It's a very nice language, and has fantastic tool support.

If you find that interesting, but Ada isn't to your taste, you can try JML for Java which provides similar (but lacking quite the same robustness and tool support) annotations. JML lets you automatically generate JUnit tests based on your annotations, and with ESC/Java2 allows for extended static checking.

If, as you appear, you are more of a fan of functional languages then I'd suggest you check out Extended ML and HasCASL which provide similar sorts of formal specification capabilities for ML and Haskell. Tool support for these is still a little limited, but they are both quite powerful and provide very expressive specification syntax.

Jedidiah.

Why does anyone take this jackass seriously?

First off, the electroplating tank:

These are a blast. Everything looks better if you electroplate it!

Any of the cool looking, under the hood gagetry for your car, found cheaply at Schuks Auto would look better in gold. Any flat sided metal object can be enhanced with whatever artwork you can make a sillouette of on your computer, print in Press-n-Peel masking material
iron on, and plate.

Flatware should never be monochromatic
Your own Electron Microscope? Sweet.

The first thing to do is find the guy that's good at operating this and buy him several good lunches. Getting good images is tricky. That done, there is a world of stuff that looks better super close up, and best yet, the annoyingly black and white nature of this device lends itself to.... Yes! Electroplate sillouttes! Imagine how cool the aluminum case sides of your favorite computer would be if this were etched on the side. Your kids/nephews could have the coolest metal lunchboxes in the school. Like this or this or this or this.
A clear spray-on enamel will keep oxidation from uglying things up if your experiment with some of the more easily tarnished metals like copper and silver....

Sounds like you're in for a good time. Good luck.

A professor at ISU (where I am) is currently doing research with eye tracking: http://hcvl.hci.iastate.edu/

The trouble with biodiesel (especially in the U.S.) is that it's usually grown in the Great Plains, and the Ogallala Aquifer, which supplies a big chunk of the Plains, is running out of water for irrigation. 1 2.

That we get 80% of our total energy from dinosaurs is my biggest concern. True, energy from dinosaurs is inexpensive, and the inefficiencies in storing large amounts of electrical energy in a portable fashion present challenges, but these are challenges we must meet while we curtail our energy consumption.

I like the idea of tapping into the energy we've put (and trapped) in the atmosphere; such an approach makes good use of existing resources.

//@ requires smsAccount.Tariff != null
//@ ensures ...
public bool CheckSmsValue(Account smsAccount) {
...
}

public class Account {
...
//@ public invariant Tariff != null
...
}

What parts do what should be clear from the names of function calls and variables, but whenever a function becomes longer than something really short, yes, it needs comments describing what happens where. If a function does something complicated, it's worth starting with a comment describing pre- and post conditions.

Now there is an excellent idea! It doesn't take a lot of effort - you should be able to come up with some basic constraints on inputs and outputs if you have any decent idea of what the function does - but it is very helpful documentation to anyone else, particularly for people who have to call the function (as it clerly delimits exactly what they need to provide, and exactly what they can expect to get back). Better yet, as long as you use a system that supports it you can get a whole lot of benefits in terms of automated checking and debugging of your code, saving you a lot of effort later.

Eiffel and D support pre and post conditions directly in the code (instead of in comments). Java has JML which is a syntax for writing pre and post conditions in comments, as well as some tools to do extra checking, add runtime checks to your code (or not) based on the conditions, write the conditions into JavaDoc properly, and automatically generate JUnit tests based on the conditions. If you program in Ada there's SPARK which supports pre and post conditions as comments as well as a range of other annotations, and provides extremely powerful tools to do extensive static checking and analysis and even generate automatically simplied proof obligations based on your annotations. If you program in Python there's PyContract which allows you to write pre and post conditions into docstrings and switch on or off runtime checking of those contracts. I expect there are plenty more, so hopefully other people can mention those.

Jedidiah.

If you're using Firefox for porn, you should check out some of the resources at the Pornzilla project. Also I highly recommend this modified linked images bookmarklet, because it's so useful and the original from Pornzilla has all the visual appeal of bleached oatmeal.

And make sure they update comments if changes necessitate it. There's nothing worse than reading through a function's description, complete with well-documented inputs/outputs/conditions/etc. and finding out that those things no longer apply because somebody changed a 1 to a 2.

That's why it's nice to have some formal semantics for inputs, outputs and conditions so that the documentation can be easily and automatically converted to, say, unittests. Take, for instance, JML which provides semantics for commenting your functions in a way that

(1) Can be used to generate automatic runtime checks for debugging
(2) Can be automatically included in your documentation
(3) Can be used to automatically generate JUnit unit tests

If you change the code but not the comment in a way that means it no longer behaves as the comment indicates... well the code will fail the unit test.

Even little things like Python's doctest module can be kind of nice, ensuring that the docstrings still represent the code they are meant to be documenting.

Jedidiah.

Blame it on JUnit. Since it provides a way to make unit testing easier, it's easier to get people to actually do it. When I was in school, we talked about unit testing, but never really did it very well. By employing the latest buzzwords such as JUnit and Spring in your design, it's much less work to build your unit tests that it would be with other languages.

At this point I'd like to point out the existence of JML, an annotation syntax and set of associated tools for Java that makes a lot of things easier and more convenient. JML allows you to do design by contract in Java and if you compile with the provided compiler jmlc it will automatically include runtime checks based on your pre and post conditions and invariants. Another tool, jmldoc, will generate JavaDoc documentation augmented with the extra specification your provided with JML annotations, making for much better documentation. You also have jmlunit which will automatically generate JUnit test classes based on your annotations.

That means you get automatically generated unit tests, the constraints of which are automatically included in your documentation (as well as in the actual code as annotations) and the option to use those constraints as runtime checks for debugging purposes. That's an awful lot of cheap benefits just for writing annotations to your code as you go.

General examples of using JML for DbC can be found here, and examples of jmlunit generating JUnit test classes can be found here.

Jedidiah.

Blame it on JUnit. Since it provides a way to make unit testing easier, it's easier to get people to actually do it. When I was in school, we talked about unit testing, but never really did it very well. By employing the latest buzzwords such as JUnit and Spring in your design, it's much less work to build your unit tests that it would be with other languages.

At this point I'd like to point out the existence of JML, an annotation syntax and set of associated tools for Java that makes a lot of things easier and more convenient. JML allows you to do design by contract in Java and if you compile with the provided compiler jmlc it will automatically include runtime checks based on your pre and post conditions and invariants. Another tool, jmldoc, will generate JavaDoc documentation augmented with the extra specification your provided with JML annotations, making for much better documentation. You also have jmlunit which will automatically generate JUnit test classes based on your annotations.

That means you get automatically generated unit tests, the constraints of which are automatically included in your documentation (as well as in the actual code as annotations) and the option to use those constraints as runtime checks for debugging purposes. That's an awful lot of cheap benefits just for writing annotations to your code as you go.

General examples of using JML for DbC can be found here, and examples of jmlunit generating JUnit test classes can be found here.

Jedidiah.

Blame it on JUnit. Since it provides a way to make unit testing easier, it's easier to get people to actually do it. When I was in school, we talked about unit testing, but never really did it very well. By employing the latest buzzwords such as JUnit and Spring in your design, it's much less work to build your unit tests that it would be with other languages.

At this point I'd like to point out the existence of JML, an annotation syntax and set of associated tools for Java that makes a lot of things easier and more convenient. JML allows you to do design by contract in Java and if you compile with the provided compiler jmlc it will automatically include runtime checks based on your pre and post conditions and invariants. Another tool, jmldoc, will generate JavaDoc documentation augmented with the extra specification your provided with JML annotations, making for much better documentation. You also have jmlunit which will automatically generate JUnit test classes based on your annotations.

That means you get automatically generated unit tests, the constraints of which are automatically included in your documentation (as well as in the actual code as annotations) and the option to use those constraints as runtime checks for debugging purposes. That's an awful lot of cheap benefits just for writing annotations to your code as you go.

General examples of using JML for DbC can be found here, and examples of jmlunit generating JUnit test classes can be found here.

Jedidiah.

This is just a research OS written in C#.

No, it's written in Sing# which is an extension of Spec# which is an extension of C#. People really ought to pay more attention to Spec# - it's a nice extension of C# that allows for more formality if and when you require it. It's in the same class of language as SPARK which is an extension of Ada, JML which extends Java with specification semantics, BitC, Extended ML, HasCASL, and I guess to a lesser extent things like Eiffel and D.

Think of it this way: static types and type signatures for functions allow you to specify things about the software that the compiler can statically check and make sure there aren't any silly errors. The languages listed above (to varying degrees) allow for more exacting specification about the software, and hence you can (with the right tools) do far more comprehensive static checking and ensure various properties of the software. The difference is that, with most of these languages, the amount of specification is optional - you can be as exacting as you want where you need it, and not bother where you don't. It's like a dynamically typed language that lets you declare and use static types (and check them)just for those areas of code where it matters (except you start with static types and can provide more exacting specification where it matters). It's well worth checking out.

Jedidiah.

As far as I can see, the language in question is not exactly "new" anymore, being C#.

Actually its an extended version of Spec# which is in turn an extension of C#. It might help to acquaint yourself with what that actually means. The first significant different is that Spec# allows for explicit pre and post conditions and other formal specificiation syntax, and hence allows for model checking, extended static checking, and formal proof if required.

It's more like someone writing an OS in BitC because it can be formally verified and hence be more secure. It does make sense, and there is good logic behind it. Comparing it to an OS in Java is just silly. Comparing it to an OS written in Java using JML and associated theorem provers is getting a little closer. Of course that doesn't address the issue of designing the OS to be more secure and reliable from the outset, and not just relying on formal verification.

If you actually bothered to read some of the material on Singularity you would see that it is an ambitious, but remarkably interesting and promising project. It is also, I would expect, something that will permanently remain buried in MS research like so many other projects. I would be interested in seeing a good open source equivalent though - such a project might have some hope of surviving.

Jedidiah.

The strict typing and verbose exception handling is annoying if you just want to get something done quick. However, if you have a large team of programmers (of varying skill levels) and a large code base, you start to appreciate that the language tries to force good programming practice, and that a lot of bugs are caught not at runtime but at compile time...This is a lot more important than raw performance, since a lot more time is spent on maintaining a product than building it in the first place (90% is number often cited).

If you feel that's the case then I suggest you consider what else you can do beyond just static types to force good programming practice and catch more bugs at compile (or verification) time. Adding some basic annotations to your code specifying, for example, preconditions and postconditions for methods, and invariant properties for classes, forces good programming practices and catches even more bugs at compile time, and can certainly make maintnenance easier.

If you're writing production code (as opposed to doing rapid prototyping) then really you ought to have a clear idea of what you intend a method to do before you write it. Given good semantics (and such thigns do exist) it isn't hard to encode those intentions formally into pre and post conditions on the method. You already do this to some extent with static types: you specify a type signature for the method; we're only really talking about having some slightly more explicit assertions about what the method does. If you're willing to do that then you automatically have much better documentation of your methods, and means to verify said documentation against the actual code you've written (by formalising the documentation), which is both good programming practice, and good for maintainability. Even better, because of the formalised statement of what the method is supposed to do, you can do some static verification akin to static type checking and catch more errors earlier.

If you like Java than check out JML which is an annotation language for Java that allows for this sort of thing. There are extra tools you can get (like ESC/Java and others) to do further static checks based on those annotations, the annotations themselves automatically get included in the JavaDocs for better documentation, and you can use the annotations to automatically generate unit tests and a testing harness for your code. That's a lot of easy wins for the little extra work of being a little bit more specific than just static types.

Jedidiah.

http://www.personalityresearch.org/papers/kooijman s.html
http://www.psychology.iastate.edu/faculty/caa/abst racts/2000-2004/01AB.pdf
http://mentalhealth.about.com/cs/familyresources/a /vidgameviolence.htm

Yea... nobody confuses the two.

Why build a nuke bomb to take care of a few cockroaches?

I guess you didn't get the memo...

Apparently, academic institutions are far better than Wikipedia. But wait! A quick Google search for the ABC shows that Department of Computer Science in Iowa State University believes the same thing: that "The Atanasoff-Berry Computer was the world's first electronic digital computer."

"....around 30,000 feet...at that altitude...temperatures of 140 degrees below freezing would kill passengers within minutes." The above, from the article, doesn't sound right. 140 degrees below freezing (assuming fahrenheit) equals a temperature of -108F(-77C), which might be a valid temperature for the tropopause over the tropics, at 50,000ft. But, at 30,000ft, it's more likely that the temperature would be about -50F(-45C), or about 80 degrees below freezing.

Actually, a guy already did:

http://www.iastate.edu/~nscentral/releases/2005/au g/hynek.shtml

http://dsc.discovery.com/news/briefs/20050829/sunh at.html

Though his primary focus was on keeping gadgets charged.
-k

Biology 101 - The characteristics of life (Iowa state uni)

In the past, I've made the argument that forcing people to declare types lowers productivity and decreases legibility.

The one good rebuttal I got was that it really helps to declare types on function parameters; it serves as a kind of documentation of the intended use and operation of a function. Plus, of course, it allows the compiler to catch errors where the function you write doesn't have the type you say it does.

I really wish using contracts (preconditions and postconditions) for this purpose would catch on. It provides better more exacting documentation of the function (not just the type on inputs and outputs, but specifics of what they must be, and what sorts of results you can expect in return), with an OO language that supports it (like Eiffel or D) it fits very naturally with inheritance (you cna weaken inherited preconditions, but not strengthen and vice versa for post-conditions), and it automatically provides an extremely powerful test harness for all your code by simply setting a switch to check all contracts at runtime.

If this sounds interesting and you program in Java, please take a look at JML and related tools. It lets you specify contracts via a JavaDoc style notation that

(1) Gets added to your javadoc documentation.
(2) Can be used to automatically generate a unit testing framework.
(3) Allows you to use extra static checking tools (like ESC/Java2) that can catch far more errors than static types alone - all prior to runtime.

If you're bothering to document your functions why not formalise the documentation a little further to allow generation of unit tests and extra static checks? It just makes sense.

Jedidiah.

Kathy will you marry me?

That's a very interesting question, and you are right, it does often seem to b conveniently ignored. I did find a couple of rather woolly links here and here. There are of course many other links , but they seem largely preoccupied with managing food, oxygen and human waste rather than actually getting the astronauts back off the Martian surface.

You can relax. There isn't a serious danger.

Current standards such as 3-DES (triple-DES) and AES require a LOT more comuputing power than that to brute force.

I've taken the Cryptography course from Iowa State University so I have a bit of information on hand from my class notes...

The best known attack against 3-DES has a complexity of 2^113. Having 20,000 nodes is about 2^14 nodes. Heck, we'll assume 32,000 nodes. so 2^15. This still has a complexity of 2^98 for each machine to handle, or 2^42 more than DES. (2^43 if you consider the complementation property of DES which reduces the complexity of DES to 2^55.)

This means it woudl still be trillions of times longer than than it took to break DES, even if every machine could have performance equal to the custom DES cracker built. I don't know about you, but I don't have trillions of days to consider the problem.

AES is even tougher to crack than 3-DES, I'm not sure if there are any new attacks, but the key-space is 128, 196 or 256 bits. Even with the smallest key, 128 bits, this is thousands of times stronger than 3-DES. (2^128 vs. 2^113)

So relax, use the latest standards to encrypt your information, and for the love of the Flying Spaghetti Monster, don't use a key that is a regular word! The way ciphers are broken today is by trying a variety of dictionary words or sentences as the key. Just like a password, make your keys random, or random in appearance.

You can relax. There isn't a serious danger.

Current standards such as 3-DES (triple-DES) and AES require a LOT more comuputing power than that to brute force.

I've taken the Cryptography course from Iowa State University so I have a bit of information on hand from my class notes...

The best known attack against 3-DES has a complexity of 2^113. Having 20,000 nodes is about 2^14 nodes. Heck, we'll assume 32,000 nodes. so 2^15. This still has a complexity of 2^98 for each machine to handle, or 2^42 more than DES. (2^43 if you consider the complementation property of DES which reduces the complexity of DES to 2^55.)

This means it woudl still be trillions of times longer than than it took to break DES, even if every machine could have performance equal to the custom DES cracker built. I don't know about you, but I don't have trillions of days to consider the problem.

AES is even tougher to crack than 3-DES, I'm not sure if there are any new attacks, but the key-space is 128, 196 or 256 bits. Even with the smallest key, 128 bits, this is thousands of times stronger than 3-DES. (2^128 vs. 2^113)

So relax, use the latest standards to encrypt your information, and for the love of the Flying Spaghetti Monster, don't use a key that is a regular word! The way ciphers are broken today is by trying a variety of dictionary words or sentences as the key. Just like a password, make your keys random, or random in appearance.

People haven't changed much since primitive times. On a day after day basis it was not possible to work on hunting more than 4 to 6 hours a day. The same remains true today, the brain can only concentrate for so long.

I recenty took a similar trip to Costa Rica where one of our jungle tour guides told us about a similar fungus that affects grasshoppers. Supprisingly, she also said that it has preformance enhancing effects when consumed by humans. No idea if this has any validity, but it is remarkablly similar to the fungus described here: Diseases are Killing Grassshoppers

agriculture is nothing but selecting food crops based on various genetic qualities

True, but (I suspect you will struggle with this) agriculture is not necessarily an unqualified good.

the hysterical uneducated ignorant peasants were out to burn a creature that only wanted to help them.

You use that analogy and describe someone else as an "propagandized"? The nicest thing I can think of to say is that you are entitled to your religious beliefs.

It's got jet engine(s) - will they produce enough power? According to this converstion table, 15 KW = 20 HP. My car has considerably more than that, and it doesn't generate anywhere near as much power as a jet engine.