A NASA Intern

One of my friends from Idaho is doing an Internship for NASA in Virginia. He wrote me an email about his orientation. I thought it was good enough to post here. So, enjoy:

Today was my first day at NASA. Langley Research Center is a quite impressive place. It's also right next to Langley Airforce Base so we see F-15 fighters fly by all day. There were 164 Scholarship students, about 30 Fellowship students, about 10 interning professors, and about 20 high school students all at the orientation. We sat through a mostly boring 3 1/2 hours of safety and security lectures. The most interesting part was the part where they talk about past, present, and future research such as the X-43, a new civilian jet/plane that can reach mach 10! That's about 7,500 mph! They also have a flying car that has been finalized for years now and ready to replace regular automobiles - the only problem is the software. The flying car needs real time networked software that works anywhere in the world and is 100% guaranteed never to fail. Good luck with that.

The funniest part was the presentation by the head IT guy. He was talking about viruses and worms and computer security and he didn't even know how to work a computer. He was pressing the right mouse button (instead of the left one) the whole time to access links on his website. A menu would pop up and he would choose "open in new window" (he's trying to go from one slide to another). He eventually had something like 40 windows on top of each other and he didn't even know it because the windows were maximized. He then wondered why the computer crashed...dooh!

I met my group and we talked a little about the project. Basically we're going to be using Python, html, Zope (which uses dtml), and Postgresql to create a web-based application to enhance SRI's Prototype Verification System (PVS, a formal methods prover) by allowing for adding, editing, and accessing of mathematical theories, functions, formulas, lemmas, etc. directly from PVS itself. Researchers from all institutions will have public access and can submit new math formulas anytime. The goal is to eventually have at least 1 million formulas in the database. So far we have about:

- 20 libraries
- 465 theories
- 1179 functions
- 3966 formulas

with the current libraries being:
prelude, bitvectors, finite sets, algebra, analysis, arrays, bags, calculus, digraphs, div, fixedpoints, graphs, mod, nat funs, number theory, powersets, reals, series, trig, and vectors

Our group's goal is to finalize the application by the end of our
internship. That's about all I know pertaining to my project. At the end we
have to submit a research paper for publication. I'm sure you're all looking
forward to reading that...

Neil.

Good Luck Neil. I hope you have fun. NASA Rules (Because they buy Boeing stuff).