- Feature Articles
- CodeSOD
- Error'd
-
Forums
-
Other Articles
- Random Article
- Alex's Soapbox
- Announcements
- Best of…
- Best of Email
- Best of the Sidebar
- Bring Your Own Code
- Coded Smorgasbord
- Mandatory Fun Day
- Off Topic
- Representative Line
- News Roundup
- Editor's Soapbox
- Software on the Rocks
- Souvenir Potpourri
- Sponsor Post
- Tales from the Interview
- The Daily WTF: Live
- Virtudyne
Admin
Conjecture: Vijay assumed unbounded precision, and did not account for the modular arithmetic arising from the constraints of the system. I have a proof for this, but it won't fit in a comment.
Admin
Or in the words of the wise Don Knuth: "Beware of bugs in the above code; I have only proved it correct, not tried it."
Admin
Yeah, that's pretty bad news alright. ;-)
Admin
Drip, drop, here comes the law of leaky abstractions...
Admin
Even if he had "proved" it correct, it takes a special kind of arrogance to assume one has managed to faithfully reproduce what is needed in code, especially in a new codebase.
I recall reading somewhere that almost no-one can write more than 9 lines of code without making at least one error, I work on the assumption I'm generally worse than that and test accordingly.
Admin
"Bad news Robert, as of this morning, Vijay will no longer be working with your group".
Oh no. carries on as normal
Admin
Sevneth
Admin
"Bad news Robert...as of this morning, Vijay will no longer be working with your group."
Since when did this site become The Daily Heartwarming Story? Normally on TDWTF it would be Robert getting fired.
Admin
I'm intrigued as to how this "proof" works.
Admin
By carefully ignoring the possibility that the real world is different from his mathematical model.
Vijay should heed Jan van de Snepscheut's famous quote "In theory, there is no difference between theory and practice. But, in practice, there is." Anybody who enters our field should be made aware that it isn't as much of an exact science as it is first supposed to be.
Admin
Quite. Compscis often have significant trouble understanding that their 1s are tapered pulses of voltage rather than discrete spikes.
Admin
Like this: Well, Vijay, of course we absolutely trust you and your proof. The problem is that if it doesn't work, we might create useless 150 ton block of steel, which will cost about $50,000. Since you are so sure and the fix is proven, I suppose you will agree to pay the cost out of your own pocket if this goes wrong?And give this in writing?
Admin
As a math major this was painful to read. That's not how math works – it's not called a "systemic science" instead of a "natural science" for a reason.
Admin
This is why I never hire based on any educational merits. Sure, they do play a part in that they studied the subject, but they always have to prove that they can turn the theory into workable practice, and quite sadly, like this, many fails spectacularely. I was interviewing one guy one day for an embedded development role, that involved writing Linux kernel drivers, and you may know, they are written in C. This guy suggested that we write the driver in Java, and he wasnt for giving up. I just could not figure out how he thought that would work, and his explanations were less than convincing, in that the computer would boot up on java, run the kernel module, that would load the kernel on top of the java, and somehow, make the system go. (inbetween the java and the loading kernel, there were some black magic steps involved). Obviously, he was not hired. My preferred choice is someone who actually understand what they are doing, and can turn it into practice, even if they don't have the full school degree jackpot. Sometimes, a lesser schooling is worth more. just saying.
Admin
Wouldn't know about a Java driver but some newer SOCs contain a port of java allowing the firmware developer to code in Java rather than c/assembly
Admin
Indeed. A healthy level of skepticism is essential for anyone in this industry... a recognition that it doesn't matter if the bug is provably impossible if the real-world evidence says otherwise.
Admin
perhaps so, but you dont write a kernel driver for linux in java.
Admin
Vijay was right, obviously. It's proven. The code is correct, it is reality that needs fixing.
Admin
TRWTF is that the US still uses the Fahrenheit scale.
Admin
Oh, -255F... Our devices have some temperature sensors, and their values are in tenth centigrades. A colleague decided to use a single byte for such a value. With the raising heat of the summer, the temperature happened to cool down rapidly - after soaring beyond 25.5°C.
Admin
I've interviewed and hired many, many developers. In almost every circumstance graduates don't make the cut (and make their shortcomings abundantly clear during the interview process). About 2/3 of them (in my experience, at least) demonstrate an attitude problem or superiority complex related to the fact that they have a degree. They are painful to manage and far less likely to be team players.
Admin
"We are the buddy bears, we always get along, and if you ever disagree then you are surely wrong..."
Admin
Forgive my ignorance if I'm sorely mistaken, but as I understand it the main reason that you wouldn't think of being able to write a kernel in java is that java programs are normally run from java byte code and interpreted by the JVM, no? But it's also possible to compile java programs into a binary executable which can be run directly without the JVM. Wouldn't that make it technically possible (if still a horrible, horrible idea)?
Admin
Embedded developer here. ;-) Yes, it is theoretically possible to write Java and have it compiled into something that can loaded onto your device. However, if the appropriate BSPs and APIs aren't available for Java, this will be pointless. Where I work, we use Java only on workstations. For our embedded work, we're mainly using C and Ada. Our firmware developers use Verilog, which would probably give the fellow in that story conniptions. :-D So the bottom line is that your development language is probably going to be dictated by the choice of hardware, operating system, and development tools.
Of course, the larger moral is that anyone who comes into maintenance of a mature codebase and starts suggesting porting it to a new language really has no clue what they're talking about. They have no idea whatsoever of the staggering level of effort they've just proposed, and in all likelihood, have only suggested the port because they're actually only comfortable in one language. In short: someone you probably shouldn't have hired.
Admin
It is technically possible to write a new kernel in Java. You can use any language you like if you're fine with extending the language. By using compiler intrinsics or other extensions that allow you to have control over the generated code, you can do what wouldn't otherwise be possible in a high-level language. There are several metacircular language implementations that use this approach.
Note that this doesn't mean that writing a Linux kernel driver in Java is possible. A normal binary produced from a JVM with ahead-of-time compilation has the code for the Java program and the parts of the runtime environment that are needed to run the program. The binary obeys Java semantics and those semantics don't match well with what the kernel expects. They certainly won't match for normal Java (e.g. garbage collection) and I doubt they'd match for realtime variants of Java.
So if you really wanted to write a Linux kernel driver in "Java", you'd have to have a runtime environment that compiles Java into a binary with the semantics expected by the kernel. So you'd translate from "Java" to C-like semantics and then have machine code with those C-like semantics. This really doesn't make any sense because you could just write in C to start with and save yourself the considerable trouble of writing your own runtime system.
Admin
First! Here it is - proven in writing.
Admin
I'm pretty sure that quote was around for a long time before it was attributed to Mr. van de Snepsheut, or the many other people it's been attributed to.
Admin
Where there’s a Vijay, there’s gonna be trouble...
Admin
You're missing the easy solution! Just rewrite Linux in Java!
Admin
"a 150 ton cake made of red-hot molten iron that's worth millions of dollars" - that's BS, the price of steel per ton is only about a couple of hundred dollars, so 150 tons of it are worth less than 100k at most...
Admin
Probably. I heard it in engineering school in the 1960s.
Admin
It's also why I'm not impressed with someone with a computer science degree. You can do a lot more with someone with practical knowledge in something that can write programs for that area, than with someone who knows everything about programming and nothing about practical application of that programming.
Admin
Have you added cost of cleaning or replacing the machines? I don't work at steel mill but I would assume that in case of failure the cost of material is insignificant compared with damages to machines - or, let's hope not, humans.
Admin
Well it could be that Vijay was correct and the simulator software had a bug.
Admin
Regarding Java and embedded -- anyone here never heard of J2ME or Java Card?
Not saying you should use them (I write my bare metal apps using C) but it's not quite as ridiculous to write Java code on embedded as people here seem to think.
Admin
The first time I heard about mathematically proven programs was when I learned the Computer Science professor had less experience in programming for a customer, internal or external than I did, and I had very little at that time. Yes it is possible to construct a mathematical model of what you think the program should do, and by carefully restricting how you code, to be able to mathematically prove that the code implements the mathematical model. There are two problems with this:
If there was a mathematical model of the program that was easier to write and validate than the code itself, why not write a compiler for that mathematical model? This may be more obvious to me because my earliest CS classes were in the 1970's when new and theoretically "better" languages like APL, Forth, and LISP were almost flavors of the month. Viewed in that light, all the languages loved by academic CS types since Algol was invented in the 1950's were attempts to create a better mathematical description of the desired program.
To make it practical to write the ,mathematical proof, I suspect that most real-world programs would have to be drastically simplified. E.g., the messy details of formatting display screens and printouts are probably omitted.
Admin
Most of you people, and Vijay, seem to live in the 20th century. You do not write proofs of software properties on paper - this is never going to work. Incidentally, there exists technology which makes it practically possible to formally verify realistic software, using a proof assistant like Coq or HOL. For now, tough, it is far from cost-effective enough to be used for ordinary software development. Vijay definitely would not be able to do it by himself overnight - it could take several man-years. No sane PhD in formal methods would ever propose to do formal software verification when coming to an "ordinary" software company. The story of this article is a complete fable.
But e.g. Intel uses HOL to verify their processors. Check out also e.g. the CompCert or seL4 projects. This technology will never rule out bugs completely because you can always have a bug in your specification, but since specifications are much simpler than actual software it significantly increases software reliability.
I would say that aside of trying to show conceit of some academics towards the "real world", the article also shows an annoying and all too common attitude of "real" software developers. That of dismissing out of hand promising tough not yet universally usable techniques, while having zero understanding of them, their current limitations and their possible future developments. That of dismissing academics, because they do some difficult stuff I don't understand, and I never heard it being used to create webpages or some other stuff I do, so it must be useless, and never will be of any use to anyone.
Admin
Logic, in general, is not executable, but it can be used to describe software. Given a logic formula specification describing program behavior, the problem of synthesizing software exhibiting this behavior is, in general, undecidable.
Not necessarily so, but it is definitely unworkable to write the proofs on paper without computer assistance. Check out CompCert or seL4 for how this can be done for some real-world software. But for now the technology of proof assistants is too much in its infancy to be industrially usable except in a few isolated critical applications, and then it still takes an enormous amount of work.
Admin
Or consider the following story.
Vijay, a newly employed CS PhD in operating systems, decided that the OS the company is using leaves much to be desired. So after a few days he came to the office with a complete code of a new OS kernel written in his notebook.
This story displays about the same level of cluelessness about modern software development as the present article displays about modern formal verification methods.
Admin
Or perhaps the story is true and Vijay had very special issues?
Admin
reminds me of the classic 1=2 "proof": http://www.quickanddirtytips.com/education/math/how-to-prove-that-1-2
Admin
It feels to me like someone has shown more intelligence than the author, and so author made up a story with the moral of "intelligence is not everything".
Admin
"reminds me of the classic 1=2 "proof" . which has a hidden divide by zero error, an incorrect proof. While proofs are not always error free, neither are the assumptions, "the givens," in proffs always error free. "Errors of the third type (solving the wrong problem) are the usual bugaboo of code proving, not errors in the proof.