A system like this sounds really useful for locating stolen cars and finding wanted criminals. It's a great idea in theory, and apparently it's effective. And if stealing a car becomes synonymous with getting caught, so much the better. But the lawsuit is also a good idea. There's no reason to build a database of "innocent" license plates. The government shouldn't be snooping on its citizens, and it's easy to imagine this information being abused. Maybe you trust this administration, but can you trust the next one, and the one after that?
Well what's the big deal? So what if a government goon knows who my friends are, how often we hang out, which political meetings I attend, whether I attend narcotics anonymous meetings or see a psichiatrist, how often I buy liquor or go to sex shops, etc. I'm nobody important, just a working stiff like everyone else. And this is all small-potatoes stuff anyhow.
But it's precisely because I'm nobody important that it isn't a big deal to me. I don't have to worry about retribution after I leak an important story about wrongdoing at my company or government agency to the media. I'm not a journalist trying to protect the confidentiality of my sources. I'm not a candidate running for office and having all my movements for the past thirty years scrutinized by the establishment party. I'm not an undercover officer or overzealous district attorney worried about being outed or targetted by the mob. These people do important work, and it's important to protect them.
The best way to prevent the database from being abused is not to build it. You can still find criminals and stolen cars, and use the system to fight crime. But citizens who haven't done anything wrong shouldn't be tracked everywhere they go, since it might be used against them for political reasons.
Well, isn't being able to eat what you want a matter of freedom? In fact, it seems to me it's more basic than most of the freedoms we talk about on slashdot.
I'd certainly like people to eat well, and I'd like the companies that produce our food to do so more ethically and with a greater concern for our well-being as consumers. But if someone wants to eat donuts and soda, that's their choice, and who am I to deny them that choice?
As a total newbie to SBCL's source code, I was delighted to find it written in Common Lisp instead of bootstrapped through some other language. The code I was interested in patching was about 30 lines total, and comments explained how it worked. Great stuff.
"Which is like saying that the primary reason the physical security industry exists is because buildings aren't naturally secure."
I think this is a bad analogy. Every building is insecure because you can always break into it, given enough force. But a computer is insecure only if it has bad programming which allows an unauthorized entity to access it.
Maybe a better analogy would be to imagine that the computer is a defendant on trial, while the attacker is a prosecutor who doesn't have sufficient evidence to convict him. The computer is secure if it avoids conviction. The prosecutor may ask questions to try to trick the defendant into incriminating himself. The defendant can either respond to these questions or say "I don't want to answer that."
The prosecutor may only ask questions and cannot torture or drug or intimidate the defendant, just as the attacker can only send packets to the computer. Clearly the defendant can always win by refusing to answer any questions, just as the computer could be disconnected from the internet or could simply drop every packet it receives. But some questions are safe to answer so the defendant might choose to respond to these, just as the computer might be willing to respond to pings or requests for public web pages. So the only way the defendant will incriminate himself is by his own stupidity, just as only an error in the computer's programming will allows it to be infiltrated.
So I think the article is basically right. A correctly programmed computer will be secure, and wouldn't need a security industry to help it. Of course, a correctly programmed computer might be even more rare than the unicorns mentioned by other posters...
I've been using a Linux desktop for about eight years and it's generally been quite nice. I have a windows machine, and I know how to use it pretty well, but I only turn it on when I want to play a game. Maybe I'm just set in my ways, but I don't think I'd enjoy using the Windows machine for much else, since I wouldn't care for not having virtual desktops and a useful shell.
But it doesn't really affect me if other people want to use Windows for their own reasons. I can still use Linux when I want to. Lots of people are constantly improving it, and I get to enjoy their efforts. I suppose if my bank stopped supporting Linux or something, that might be irritating, but it seems that the trend has been for more people to support Firefox since it's gaining traction on Windows, so it probably won't happen.
DARPA and the NSA are devoutly, religiously paranoid about computers, and they dominate the funding of computer science research. I'm sure they think they stuff like this is important, regardless of whether it is or not.
"This immediately excludes building devices that need to assure overall system integrity (from fair network gaming through to voting machines)"
I don't see why it would prevent you from developing voting machines based on GPL'd code. I mean, who cares if Joe Hacker can see and make their own versions of the voting software, as long as he can't install it on the voting machines on election day. This is a social problem of having safeguards and procedures, not a question of open or closed sources.
That's some old advice a professor gave to a friend of mine in a similar circumstance. The rationale was allegedly something about where the funding is.
"The prevalence of food insecurity was 11.9 percent in 2004, up from 11.2 percent in 2003. The prevalence of food insecurity with hunger was 3.9 percent in 2004, up from 3.5 percent in 2003."
If we assume 300 million people in the US with an even distributed amongst its households, that's 35.7 million Americans who were on the brink of not being able to afford food, with 11.7 million literally going hungry.
1. Nobody knows what they're doing. Never trust anyone who is sure that they know what they are doing when it comes to money, including me. A "balanced portfolio" is just code for "at least I will only be partially wrong."
2. Keep a record. Use a simple program (GNUCash, Quicken, whatever) to track your finances. Just keeping a record of what you spend will be pretty valuable. Buy things with a debit/credit card instead of cash when you can, so you don't forget what you bought.
3. Don't worry yet. Unless you have a whole lot of money in the bank, what you do with it right now hardly matters. That is, to a large degree, what difference does it make if you save an extra $1000 during your college career if you'll be making $50k or $100k or whatever your field pays when you leave. You'll suit yourself better in the long run by focusing on doing well in school, impressing your professors, taking that internship, and making that name for yourself than working right now if you don't need to, etc.
4. Don't listen to #3. The point of investing right now isn't to do well at it, it's to learn about it so that once you start making $50-$100k or whatever your field pays, you can invest your money more wisely than you could today. Wells Fargo has a pretty painless service called ShareBuilder that will let you buy some stocks if you want.
5. Don't listen to #4. Your major expense after college will probably be a house, and you'll probably want to be focused on saving towards that. This means you'll want to have money available when you graduate, so don't invest substantially in anything very risky or long term. CDs are probably a good option, but you could toy with some stocks.
6. Think short term. It doesn't make sense to try to save for retirement yet, since that's so far away. If you are disciplined, you'll be better served by quickly owning your own home than trying to pay it off slowly and saving for retirement at the same time. You can take up to $10,000 out of your IRA penalty-free towards the purchase of your first home, so you might want to make use of the tax advantages there. You can start seriously saving for your IRA when you get a real job.
7. Live cheaply. It's easier now than it will be later. You don't have any dependents yet, so you will only have to answer to yourself if you decide to eat rice and peanut butter for a month. Do you really need that car? Are you at home enough to even watch cable? Do you really need that cell phone?
8. Steal. Can't you use the free, nationwide LINKSYS or DEFAULT network for your internet access? Do you really need to buy that CD? [My lawyer points out that this is a joke, and I would never recommend doing anything illegal.]
9. Cheat. Sharing expenses is a lot more effective than trying to reduce your own expenses on your own. With a roommate or significant other of your persuasion, you can significantly cut your share of the rent and utilities, leaving more to save. You might even be able to share cars, computers, phones, and so forth.
10. Earn. It's a lot easier to save money when you're making lots of it. If you are working, make sure it's paying what you can get for your abilities. If you aren't, try to find a part-time job that will be a steady income, apply for scholarships, etc.
11. Enjoy #7-10 in moderation. Remember #3. Isn't it worth it to live in the dorms, even if they cost a bit more? And so forth.
For me it's a really wonderful thing. I'm going to be starting my fourth year this fall.
Financially, I have a research assistantship which pays me well enough that, if I were single, I could afford an apartment, car, and the occasional computer. Since I'm married to a CPA, and we live fairly cheaply, we've been able to build up a good amount of money over the last few years and might even have enough to buy a house when I finish. I'm sure I could make more in industry, but I wouldn't even consider it because of the work and the freedom. (NOTE: if you aren't in CS, the money might not be so good. As someone once advised a math-oriented friend of mine, "do what you want, and call it computer science.")
Some of the classes were really rewarding, and others were not so useful. I finished with all the coursework in 2.5 years, and being done has given me a lot of time to focus on my research. I work a lot. I used to play a lot of computer games, but now I mostly work instead. It's not hard to get motivated about my awesomely cool dissertation project, which I'll be proposing soon.
We have a group that works on the same kind of projects, and I get to hear what other people are working on and present my work on occasion in our weekly meetings. I have written some papers and gotten to present them at conferences, and this has let me meet a lot of people from industry. I've gotten to take summer internships in industry and in a national laboratory, and passed up a repeat internship this summer to focus on my own work. I get the feeling that, when I am done, I'll be able to choose wherever I want to work from the companies that deal with my topic.
I make my own hours, I have tons of freedom. My adviser is not much like a "boss" -- it's almost like he's working for me. His focus is on how he can help me, and how he can challenge me to make my research better. He doesn't bother me with deadlines or grunt work. I'm surrounded by smart people, and that's really wonderful. I can use the campus gym and enjoy the campus culture and, er... scenery. I'm encouraged to publish about my work and make it free software.
I didn't mind working for a company during my internships. I'm sort of anti-corporate politically, but I didn't find anything in it to be "soul-crushing". Certainly in the corporate world you had to focus on their projects, and on how you could contribute to them. I think academics get to follow interesting tangents more easily, and aren't really "managed" as much. But really I have no complaints -- I was pretty free to do what I wanted, and I liked my job during the summer. But I will say that, for whatever reason, I was really happy when it was over. I literally ran to my car when I left on my last day, and sang on the drive back home.
I don't think it's for everyone. You need to be... passionate about what you are interested in, and devoted to it, and willing to do a lot of work and stick with it. You have to be willing to give up the bigger salary, etc. And you need to be really self motivated and optimistic. If that sounds good, and you're bright, I can't think of anything that's better. Maybe starting your own company, but then you have to do something useful.:)
Inkscape 0.43 has a nice export to.eps feature. It's still sort of clunky to use, and the fonts don't always come out quite the same, but I like it a lot better than xfig. Not sure what else I can use for this sort of thing. Looking forward to 0.44.
"Ultimately, if I or you, or ABC Giant Corporation(tm) pays for the infrastructure and owns the equiptment, don't they have the right to charge as they see fit for access? If I run a dry-cleaner can't I charge more for same-day service?"
If you "dry cleaning" business is unreasonable, I can go somewhere else. But in the US there are generally only one or two choices for a usable internet connection (broadband). There simply is no competititon in the "I think I'll take my money elsewhere, thanks." sense.
Without competition to keep you honest, what is left? Only your customers' collective ability to resist you, and the government's ability to regulate you. Internet users can't resist very well; the ISPs have fought against efforts to create competition like municipal wireless projects. And, the government has chosen not to regulate. So, as a consumer, your options now are either (1) don't have internet access, or (2) pay more.
It sucks. It's as if your power company said, "We're raising the rates because our shareholders would like more money. You can't do anything about it, since there are no other power companies in town, and you need electricity."
And lets be honest: we'll all just live with it. Fighting is too much work.
"I don't understand why people still are using PDF when dvi is much better."
I use LaTeX as much as the next grad student (maybe more), but I still convert everything to PDF before posting it online or emailing it to anyone. I think it's easier for most people to open PDF files because they run into them so often that they are forced to deal with them.
Maybe I'm part of the problem, and by posting PS/DVI-only I would help to encourage the adoption of other formats. After all, few things irk me as much as the "copy protection" on the fill-in PDF tax forms, which prevents me from saving an editable copy of my taxes. I think I had this problem on both NE and IA returns this year.
Of course, those fill-in tax PDFs are really terrible in a number of ways. I remember not being able to enter the middle part of my SSN since the form wouldn't accept a leading zero. Also, in 2006, it's a little boggling that the forms don't do the arithmetic for you...
"The problem is that the formal specification is just as or even more complicated to read and write than the implementation itself."
Certainly not all is roses with formal verification. Few people have the mathematical background, experience, desire, time, etc. to make much use of formal verification, and even experts have to do a lot of work to prove anything interesting about real programs, and expertise + time is costly.
But, I don't agree that specifications are, on the average, as complicated as their implementations.
For example, imagine a system for implementing a potentially very large but sparse array. It might be quite complex in order to be efficient. But its interface might be quite simple (i.e., "load" and "store"), and correctness properties might be very succinctly stated, e.g.,
load(addr1,store(addr1,val,mem)) = val,
addr1 != addr2 -> load(addr1,store(addr2,val,mem)) = load(addr1,mem)
store(addr1,load(addr1,mem),mem) = mem
store(addr1,val1,store(addr1,val2,mem)) = store(addr1,val1,mem)
addr1 != addr2 -> store(addr1,val1,store(addr2,val2,mem)) = store(addr2,val2,store(addr1,val1,mem))
In cases where properties like these are not easy to state or prove, it may still be possible to show that some convoluted but efficient program behaves the same as another program which is very simple but would be too inefficient to use. These sorts of proofs add a lot of value, because you can now just consider the correctness of the simple but inefficient program.
"Arguably it's not really relevant either. "proving" a software program only proves that the programs conforms to the spec. Now who proves the spec? And who proves the proof?"
Specifications are often simpler than programs. As a pedagogical example, the notions of "ordered" and "permutation" are simpler to express than the code for most sorting algorithms.
In the case of operating systems, you might not even be interested in total correctness. For example, you might only try to prove something like "every process eventually gets a chance to run", instead of trying to show that they all run in some particular order.
As far as who proves the proof goes, I suppose you could have humans look at it. But probably it's more useful to write a tool. All programmers are used to working with type systems now, and your type checker is really a very simple theorem prover. More general purpose provers, such as ACL2, HOL, COQ, and PVS, can also be used to check proofs, so that not many humans need to read or understand them.
You might find it useful to think of proofs as "really good test suites" that are able to check some property not just on a few random cases, but on an infinity of cases. They may certainly take a lot more expertise and effort to set up than your typical regression suite, but they can be a lot more comprehensive, through the awesome power of induction and symbolic reasoning to reduce the infinite to the finite.
Lastly, speaking from experience, the process of proving code correct often reveals lots of hard to find bugs. Maybe they could be found in other ways, but maybe not.
Slashdot Mirror
If Colbert wins the presidency, he'll by definition be in a lot of trouble. I sure wouldn't want that job.
500 GB hard drives are now going for $100, so that 140 KB of executable bloat costs you about .003 cents.
I, for one, wouldn't worry.
I have a hard time imagining $20,000 of mandatory, non-tuition costs per year. Care to provide some more details?
Even your average dropout probably realizes $1000 isn't much.
If a guy was waving a gun put the window of a car, should it be illegal for police to pull that person over without a warrant?
But of course, and welcome to Texas!
A system like this sounds really useful for locating stolen cars and finding wanted criminals. It's a great idea in theory, and apparently it's effective. And if stealing a car becomes synonymous with getting caught, so much the better. But the lawsuit is also a good idea. There's no reason to build a database of "innocent" license plates. The government shouldn't be snooping on its citizens, and it's easy to imagine this information being abused. Maybe you trust this administration, but can you trust the next one, and the one after that?
Well what's the big deal? So what if a government goon knows who my friends are, how often we hang out, which political meetings I attend, whether I attend narcotics anonymous meetings or see a psichiatrist, how often I buy liquor or go to sex shops, etc. I'm nobody important, just a working stiff like everyone else. And this is all small-potatoes stuff anyhow.
But it's precisely because I'm nobody important that it isn't a big deal to me. I don't have to worry about retribution after I leak an important story about wrongdoing at my company or government agency to the media. I'm not a journalist trying to protect the confidentiality of my sources. I'm not a candidate running for office and having all my movements for the past thirty years scrutinized by the establishment party. I'm not an undercover officer or overzealous district attorney worried about being outed or targetted by the mob. These people do important work, and it's important to protect them.
The best way to prevent the database from being abused is not to build it. You can still find criminals and stolen cars, and use the system to fight crime. But citizens who haven't done anything wrong shouldn't be tracked everywhere they go, since it might be used against them for political reasons.
Well, isn't being able to eat what you want a matter of freedom? In fact, it seems to me it's more basic than most of the freedoms we talk about on slashdot.
I'd certainly like people to eat well, and I'd like the companies that produce our food to do so more ethically and with a greater concern for our well-being as consumers. But if someone wants to eat donuts and soda, that's their choice, and who am I to deny them that choice?
As a total newbie to SBCL's source code, I was delighted to find it written in Common Lisp instead of bootstrapped through some other language. The code I was interested in patching was about 30 lines total, and comments explained how it worked. Great stuff.
"Which is like saying that the primary reason the physical security industry exists is because buildings aren't naturally secure."
I think this is a bad analogy. Every building is insecure because you can always break into it, given enough force. But a computer is insecure only if it has bad programming which allows an unauthorized entity to access it.
Maybe a better analogy would be to imagine that the computer is a defendant on trial, while the attacker is a prosecutor who doesn't have sufficient evidence to convict him. The computer is secure if it avoids conviction. The prosecutor may ask questions to try to trick the defendant into incriminating himself. The defendant can either respond to these questions or say "I don't want to answer that."
The prosecutor may only ask questions and cannot torture or drug or intimidate the defendant, just as the attacker can only send packets to the computer. Clearly the defendant can always win by refusing to answer any questions, just as the computer could be disconnected from the internet or could simply drop every packet it receives. But some questions are safe to answer so the defendant might choose to respond to these, just as the computer might be willing to respond to pings or requests for public web pages. So the only way the defendant will incriminate himself is by his own stupidity, just as only an error in the computer's programming will allows it to be infiltrated.
So I think the article is basically right. A correctly programmed computer will be secure, and wouldn't need a security industry to help it. Of course, a correctly programmed computer might be even more rare than the unicorns mentioned by other posters...
I don't know why anyone cares about this.
I've been using a Linux desktop for about eight years and it's generally been quite nice. I have a windows machine, and I know how to use it pretty well, but I only turn it on when I want to play a game. Maybe I'm just set in my ways, but I don't think I'd enjoy using the Windows machine for much else, since I wouldn't care for not having virtual desktops and a useful shell.
But it doesn't really affect me if other people want to use Windows for their own reasons. I can still use Linux when I want to. Lots of people are constantly improving it, and I get to enjoy their efforts. I suppose if my bank stopped supporting Linux or something, that might be irritating, but it seems that the trend has been for more people to support Firefox since it's gaining traction on Windows, so it probably won't happen.
While it's fun to talk about Bush being stupid, I think a better explanation is malice.
"CNET thinks this is no punishment at all"
He hardly did anything. Being grounded for two months seems pretty reasonable.
DARPA and the NSA are devoutly, religiously paranoid about computers, and they dominate the funding of computer science research. I'm sure they think they stuff like this is important, regardless of whether it is or not.
"This immediately excludes building devices that need to assure overall system integrity (from fair network gaming through to voting machines)"
I don't see why it would prevent you from developing voting machines based on GPL'd code. I mean, who cares if Joe Hacker can see and make their own versions of the voting software, as long as he can't install it on the voting machines on election day. This is a social problem of having safeguards and procedures, not a question of open or closed sources.
but call it Computer Science."
That's some old advice a professor gave to a friend of mine in a similar circumstance. The rationale was allegedly something about where the funding is.
"Sure, $5.15/hr sucks compared to $25.15, but $5.15 can still buy a roof and constant nutrition."
I won't try to address the cost of housing. But, from http://www.ers.usda.gov/briefing/FoodSecurity/:
"The prevalence of food insecurity was 11.9 percent in 2004, up from 11.2 percent in 2003. The prevalence of food insecurity with hunger was 3.9 percent in 2004, up from 3.5 percent in 2003."
If we assume 300 million people in the US with an even distributed amongst its households, that's 35.7 million Americans who were on the brink of not being able to afford food, with 11.7 million literally going hungry.
1. Nobody knows what they're doing. Never trust anyone who is sure that they know what they are doing when it comes to money, including me. A "balanced portfolio" is just code for "at least I will only be partially wrong."
2. Keep a record. Use a simple program (GNUCash, Quicken, whatever) to track your finances. Just keeping a record of what you spend will be pretty valuable. Buy things with a debit/credit card instead of cash when you can, so you don't forget what you bought.
3. Don't worry yet. Unless you have a whole lot of money in the bank, what you do with it right now hardly matters. That is, to a large degree, what difference does it make if you save an extra $1000 during your college career if you'll be making $50k or $100k or whatever your field pays when you leave. You'll suit yourself better in the long run by focusing on doing well in school, impressing your professors, taking that internship, and making that name for yourself than working right now if you don't need to, etc.
4. Don't listen to #3. The point of investing right now isn't to do well at it, it's to learn about it so that once you start making $50-$100k or whatever your field pays, you can invest your money more wisely than you could today. Wells Fargo has a pretty painless service called ShareBuilder that will let you buy some stocks if you want.
5. Don't listen to #4. Your major expense after college will probably be a house, and you'll probably want to be focused on saving towards that. This means you'll want to have money available when you graduate, so don't invest substantially in anything very risky or long term. CDs are probably a good option, but you could toy with some stocks.
6. Think short term. It doesn't make sense to try to save for retirement yet, since that's so far away. If you are disciplined, you'll be better served by quickly owning your own home than trying to pay it off slowly and saving for retirement at the same time. You can take up to $10,000 out of your IRA penalty-free towards the purchase of your first home, so you might want to make use of the tax advantages there. You can start seriously saving for your IRA when you get a real job.
7. Live cheaply. It's easier now than it will be later. You don't have any dependents yet, so you will only have to answer to yourself if you decide to eat rice and peanut butter for a month. Do you really need that car? Are you at home enough to even watch cable? Do you really need that cell phone?
8. Steal. Can't you use the free, nationwide LINKSYS or DEFAULT network for your internet access? Do you really need to buy that CD? [My lawyer points out that this is a joke, and I would never recommend doing anything illegal.]
9. Cheat. Sharing expenses is a lot more effective than trying to reduce your own expenses on your own. With a roommate or significant other of your persuasion, you can significantly cut your share of the rent and utilities, leaving more to save. You might even be able to share cars, computers, phones, and so forth.
10. Earn. It's a lot easier to save money when you're making lots of it. If you are working, make sure it's paying what you can get for your abilities. If you aren't, try to find a part-time job that will be a steady income, apply for scholarships, etc.
11. Enjoy #7-10 in moderation. Remember #3. Isn't it worth it to live in the dorms, even if they cost a bit more? And so forth.
At my school it's covered as part of your Teaching or Research Assistant position.
For me it's a really wonderful thing. I'm going to be starting my fourth year this fall.
:)
Financially, I have a research assistantship which pays me well enough that, if I were single, I could afford an apartment, car, and the occasional computer. Since I'm married to a CPA, and we live fairly cheaply, we've been able to build up a good amount of money over the last few years and might even have enough to buy a house when I finish. I'm sure I could make more in industry, but I wouldn't even consider it because of the work and the freedom. (NOTE: if you aren't in CS, the money might not be so good. As someone once advised a math-oriented friend of mine, "do what you want, and call it computer science.")
Some of the classes were really rewarding, and others were not so useful. I finished with all the coursework in 2.5 years, and being done has given me a lot of time to focus on my research. I work a lot. I used to play a lot of computer games, but now I mostly work instead. It's not hard to get motivated about my awesomely cool dissertation project, which I'll be proposing soon.
We have a group that works on the same kind of projects, and I get to hear what other people are working on and present my work on occasion in our weekly meetings. I have written some papers and gotten to present them at conferences, and this has let me meet a lot of people from industry. I've gotten to take summer internships in industry and in a national laboratory, and passed up a repeat internship this summer to focus on my own work. I get the feeling that, when I am done, I'll be able to choose wherever I want to work from the companies that deal with my topic.
I make my own hours, I have tons of freedom. My adviser is not much like a "boss" -- it's almost like he's working for me. His focus is on how he can help me, and how he can challenge me to make my research better. He doesn't bother me with deadlines or grunt work. I'm surrounded by smart people, and that's really wonderful. I can use the campus gym and enjoy the campus culture and, er... scenery. I'm encouraged to publish about my work and make it free software.
I didn't mind working for a company during my internships. I'm sort of anti-corporate politically, but I didn't find anything in it to be "soul-crushing". Certainly in the corporate world you had to focus on their projects, and on how you could contribute to them. I think academics get to follow interesting tangents more easily, and aren't really "managed" as much. But really I have no complaints -- I was pretty free to do what I wanted, and I liked my job during the summer. But I will say that, for whatever reason, I was really happy when it was over. I literally ran to my car when I left on my last day, and sang on the drive back home.
I don't think it's for everyone. You need to be... passionate about what you are interested in, and devoted to it, and willing to do a lot of work and stick with it. You have to be willing to give up the bigger salary, etc. And you need to be really self motivated and optimistic. If that sounds good, and you're bright, I can't think of anything that's better. Maybe starting your own company, but then you have to do something useful.
Ah. Yeah I usually use both regular latex and pdflatex.
.pdf from an .eps using "epstopdf".
.svg file into your subversion repository, and your makefile can generate everything else.
But it's quite easy to create a
epstopdf foo.eps
And in fact you can generate the EPS from the command line too:
inkscape foo.svg -E foo.eps
So you only need to put the
Inkscape 0.43 has a nice export to .eps feature. It's still sort of clunky to use, and the fonts don't always come out quite the same, but I like it a lot better than xfig. Not sure what else I can use for this sort of thing. Looking forward to 0.44.
"Ultimately, if I or you, or ABC Giant Corporation(tm) pays for the infrastructure and owns the equiptment, don't they have the right to charge as they see fit for access? If I run a dry-cleaner can't I charge more for same-day service?"
If you "dry cleaning" business is unreasonable, I can go somewhere else. But in the US there are generally only one or two choices for a usable internet connection (broadband). There simply is no competititon in the "I think I'll take my money elsewhere, thanks." sense.
Without competition to keep you honest, what is left? Only your customers' collective ability to resist you, and the government's ability to regulate you. Internet users can't resist very well; the ISPs have fought against efforts to create competition like municipal wireless projects. And, the government has chosen not to regulate. So, as a consumer, your options now are either (1) don't have internet access, or (2) pay more.
It sucks. It's as if your power company said, "We're raising the rates because our shareholders would like more money. You can't do anything about it, since there are no other power companies in town, and you need electricity."
And lets be honest: we'll all just live with it. Fighting is too much work.
"I don't understand why people still are using PDF when dvi is much better."
I use LaTeX as much as the next grad student (maybe more), but I still convert everything to PDF before posting it online or emailing it to anyone. I think it's easier for most people to open PDF files because they run into them so often that they are forced to deal with them.
Maybe I'm part of the problem, and by posting PS/DVI-only I would help to encourage the adoption of other formats. After all, few things irk me as much as the "copy protection" on the fill-in PDF tax forms, which prevents me from saving an editable copy of my taxes. I think I had this problem on both NE and IA returns this year.
Of course, those fill-in tax PDFs are really terrible in a number of ways. I remember not being able to enter the middle part of my SSN since the form wouldn't accept a leading zero. Also, in 2006, it's a little boggling that the forms don't do the arithmetic for you...
"The problem is that the formal specification is just as or even more complicated to read and write than the implementation itself." Certainly not all is roses with formal verification. Few people have the mathematical background, experience, desire, time, etc. to make much use of formal verification, and even experts have to do a lot of work to prove anything interesting about real programs, and expertise + time is costly. But, I don't agree that specifications are, on the average, as complicated as their implementations. For example, imagine a system for implementing a potentially very large but sparse array. It might be quite complex in order to be efficient. But its interface might be quite simple (i.e., "load" and "store"), and correctness properties might be very succinctly stated, e.g., load(addr1,store(addr1,val,mem)) = val, addr1 != addr2 -> load(addr1,store(addr2,val,mem)) = load(addr1,mem) store(addr1,load(addr1,mem),mem) = mem store(addr1,val1,store(addr1,val2,mem)) = store(addr1,val1,mem) addr1 != addr2 -> store(addr1,val1,store(addr2,val2,mem)) = store(addr2,val2,store(addr1,val1,mem)) In cases where properties like these are not easy to state or prove, it may still be possible to show that some convoluted but efficient program behaves the same as another program which is very simple but would be too inefficient to use. These sorts of proofs add a lot of value, because you can now just consider the correctness of the simple but inefficient program.
"Arguably it's not really relevant either. "proving" a software program only proves that the programs conforms to the spec. Now who proves the spec? And who proves the proof?"
Specifications are often simpler than programs. As a pedagogical example, the notions of "ordered" and "permutation" are simpler to express than the code for most sorting algorithms.
In the case of operating systems, you might not even be interested in total correctness. For example, you might only try to prove something like "every process eventually gets a chance to run", instead of trying to show that they all run in some particular order.
As far as who proves the proof goes, I suppose you could have humans look at it. But probably it's more useful to write a tool. All programmers are used to working with type systems now, and your type checker is really a very simple theorem prover. More general purpose provers, such as ACL2, HOL, COQ, and PVS, can also be used to check proofs, so that not many humans need to read or understand them.
You might find it useful to think of proofs as "really good test suites" that are able to check some property not just on a few random cases, but on an infinity of cases. They may certainly take a lot more expertise and effort to set up than your typical regression suite, but they can be a lot more comprehensive, through the awesome power of induction and symbolic reasoning to reduce the infinite to the finite.
Lastly, speaking from experience, the process of proving code correct often reveals lots of hard to find bugs. Maybe they could be found in other ways, but maybe not.