Well, it certainly is a good thing that they try to put this language on a solid basis. It is used in far too many places to remain without a specification.
They are not. In fact, not at all. Most of mathematics is done informal, yet exact. Of course some intelligence is required on the side of the user and the writer.
They are not. But it takes some _actual_ understanding to see that.
I have to say I find Java apologist like you not only pathetic but repulsive. This "language" represents everything that is wrong with "modern" software creation. It is so badly designed, you cannot handle the sources without tools. It is so full of syntactic clutter, it is barely readable. It is so badly non-orthogonal, code re-use is a myth. Even badly written C or Perl is better. It is so slow and resource-hungry, that when you deliver some good-quality C-code that does the same, some people only believer your performance numbers after they see it in action. And it is so badly structured, that most Java "programmers" do not even understand most Java mechanisms. Java code is always incredibly bloated and incredibly hard to read and universally 10...100 times longer than it needs to be. It often solves problems that have already be solved in an universal way and does it badly.
Really, if somebody claims to be a "Java programmer", the assumption that they are fundamentally incompetent with regard to CS concepts, cannot do anything in any other language, have zero understanding for operating systems and that their Java code is badly borked is almost a certainty.
You very likely have used not a single language that has a formal specification. That is because there is not a single mainstream language that has one. The only language with a formal specification I know is Algol68.
And "fail to read plain English". The C standard is not a formal specification at all. It is a formal standard though. A formal standard is made formal by a formal standardization process. A formal specification is made formal by exclusive use of a formal specification language. Hint: "formal" means two different things here.
Sessh, does nobody know any basic CS terminology anymore?
Is somebody promises a "formal specification" they promise something very, very specific. In practice, you usually only need a "specification" and in fact, as I wrote before, a formal specification is typically pretty useless. People just should not try to inflate the perceived quality of their product by using words they do not understand.
You have obviously never done this. Pathetic. And no, we are not reviewing "our" software, quite obviously. If you knew the first thing about professional code review, you would know that coders and reviewers must never be the same or closely connected.
You whole statement was possibly meant to drip irony, but it only drips confusion.
A formal specification is a specification done in a formal specification language. There is no other meaning of that term.
What, there are language specs that don't have an EBNF or similar for valid statements in the language? Seems odd.
If you had the least clue what you are talking about (or actually had read what I wrote), you would know that there are informal specifications around and that this is in fact the normal way to do them. You would also know that putting in some formal grammar does not make a specification a formal one.
theory, you could check a formal specification for soundness using an automated theorem prover
Ooh, sounds magical. Let me know when you find a theorem prover that is (even "in theory") complete and consistent (and runs in finite time).
You throw around big words but do not understand them. Pathetic.
I am not confused at all. I never wrote "formal language", I wrote "formal specification language", which is a completely different beast. You fail.
It is "as formal as in a formal specification language" exactly if it is done in a formal specification language. There really is no other way. And yes, "formal" is very much the central and most important point if somebody claims to have a formal specification. The "formal" is not a modifier to "specification", a "formal specification" is one very specific thing. I think you have no clue what "formal" actually means. Your second paragraph demonstrates that. Maybe stop commenting on things you do not understand?
And anyways, have you read what I wrote above? At the very least you have not understood it. Let me re-iterate: "Formal" and "exact" are orthogonal concepts. Of course, you have to understand both to see that.
ddd? Not needed in most cases, unless you have created a mess. Also pretty hard to use if you only have a text-terminal. Plain GDB is actually pretty good.
It has gotten so bad, that if you are competent, you can actually code everything, excluding only the most standard libraries from scratch in the time it takes to get the components under control. Of course, using components leads to bloat, unwanted functionality (i.e. security problems), slow speed and low maintainability. Yet more and more people seem to be incapable of doing anything else.
Really, that is completely ass-backwards. We do not need better tools. We need better programmers. I recently finished a medium sized project in C, using text editor, command-line compiler, commandline-debugger and svn only, and I found absolutely nothing wanting in my tool-chain. That was dual-platform development on Linux and Solaris (with the Solaris compiler and debugger on Solaris, not the GNU tools), and still, even an unified IDE would have benefited me almost nothing.
Now, it may be that I am stuck in the dark ages of programming, but I don't think so. My development speed and result quality is entirely appropriate and significantly better than average. However, I have observed that many "programmers" are indeed helpless without exactly the complex tool-chain they are used too and cannot even produce simple code without the only IDE they know. These people have no business producing software and, indeed, they do not understand the language they code in or the machine they code for. They "muddle through" somehow, having their hand held by the IDE. It seems these people are the norm, not the exception. It is really no surprise so much software is so bad.
The idea that the IDE becomes _necessary_ to access the code is spot on. We do code security reviews as part of our work, and, for example, most Java projects cannot be reviewed anymore without the Eclipse set-up that was used to produce them. That is pure insanity!