Introduction to Ada and SPARK (2009) [pdf]
cse.msu.edu
cse.msu.edu
"Affects" there is clearly a noun, thus meaning "the conscious subjective aspect of feeling or emotion" (thank you, WordNet!). So, Ada is artificially intelligent?!?!
(I consider the authors to be a legitimate mocking target because they're supposed to be talking about a formal method; details matter.)
Anyway, I'd like to point out that most, if not all, of what was left out of Ada can, in fact, be handled formally with more or less difficulty. Some are trivial, such as goto's, while others are pretty damn hairy, like pointers and dynamic memory. One that is particularly galling is concurrency, where "Cannot reason about the effects of a [concurrent] module by examining its code in isolation" is simply false although nondeterminacy does remain problematic.
Overall, I think I like the SPARK approach, although I've never dug into it in detail.
Systems integration projects routinely fail in the military community, and the reason for this, of course, must be purely the result of so many different programming languages! Anyone who has worked in that industry can tell you that the problem Ada was trying to solve wasn't the actual problem.
Limited number of available programmers due to absurdly arbitrary security clearance process: Check Highly bureaucratic culture which has multiple middle managers for every person who actually works: Check Contract award process which is so complex that it favors proposal writing skills over software writing skills: Check Bloated fiefdoms whose members actively fight any and all efforts to integrate to protect their own jobs: Check
None of these problems are ever going to be solved by a programming language.
I am coincidentally researching if I could rewrite parts of a personal project in Ada (from C) to improve reliability, and so far have failed to conclude either way.
Ada/SPARK have merit if you really want to do hard real time and formal methods. That seems overkill for a personal project?
It's possible to run L4 processes written in SPARK on top of seL4.
It may be easier to just generate binary code from assembly in coq (as Microsoft Research has demonstrated: http://research.microsoft.com/en-us/um/people/nick/coqasm.pd...) instead of trying to shoehorn a C compiler into a verified context and then running proofs over that for non-trivial problems.
seL4 was a huge project. Once you start reasoning about using L4 APIs, it will only become worse (eg. it's not simple to determine who has access to the pages in any L4 AddressSpace)
Frama-C might be worth looking into if the goal is improved reliability, and they'd be able to leverage their existing C skillset.
The MISRA documentation is not very expensive and useful by itself, £15 + VAT for an ecopy: http://www.misra.org.uk/?TabId=58
There is a blog post about rewriting a drones control system in Spark if you were curious: http://blog.adacore.com/how-to-prevent-drone-crashes-using-s...
It does exactly what you were planning. Taking C code and rewriting it in Spark in an embedded environment.
Indeed but that wasn't the intention, the problem that the DoD had was that disparate systems with decade long service lives written in a huge variety of languages was going to cost them more and many of those languages where relatively unsafe languages.
Ada was built as a safer systems language that could replace many of those prior languages, a role it very much succeeded in - dysfunctional organisations are going to be dysfunctional whatever language you use but that doesn't stop one language been "safer" (against a given set of metrics) than another.
Lots of modern systems are still written in C or C++ but largely because of organisational/real world reasons (availability of programmers fluent in those languages, the sheer complexity of modern systems, you can argue that writing Ada on top of a Linux kernel might not be the sanest choice).
Ada still has it's niche though and if nothing else it showed that a language can be designed with safety in mind and it also prototyped many of the features that cropped up in later languages.
Algol already showed that in the mid-60s, check Burroughs computers for example.
It was the C designers that decided to ignore safety.
Team UNIX(TM) continued that approach, since they also had meager computers to start with, a PDP-7 with I suspect not a lot of memory, then a PDP-11(/20) with the extra memory bank option, then a PDP-11/45, which while a big and fast minicomputer in it's day, still only allowed 64 KiB of instructions, 48 KiB of data, and 8 KiB of stack for a program (the latter was the usual way to split up data space with its 8 KiB page MMU).
Just as info, here is the brochure of the B5000 from 1961.
http://www.cs.virginia.edu/brochure/images/manuals/b5000/bro...
Ada by the way is alive and kicking; nowadays it's known as PL/SQL in Oracle.
Something on my long list of things to play with when I have time :).
As far as the proposal writing goes, if a group can't draft a decent proposal, how are they going to produce good documentation? I'm not seeing how grantsmanship presents an unfair bar here.
In practice, having a security clearance becomes a job requirement of the same level as experience and ability to perform the job. Since cleared jobs don't pay several times more than jobs without the requirement and there's no way for an individual to get a clearance without the sponsorship of an employer, job-related skill tends to suffer.
Government contracts are a very specialized skillset[1] that is completely unrelated to any kind of development effort. People with that skillset bring in revenue and are thus assets; people doing development are expenses.
No, but they do offer career security, i.e. not having to become a consultant or whatever if you're not a superstar when you turn ~40. I've also have a couple of acquaintances with high level security clearances, and they can talk about the tools they use, and at least in their cases they're not radically different than what's normally used outside that world. E.g. Sun gear back in the '90s when it was the best, C#, Java, various generally obscure document imaging tools that are standard in the field, etc. And plenty of FOSS, the government loves it, or at least the intelligence agencies do.
If the people doing development are working on a cost plus basis, they're anything but an "expense", they're youe lifeblood. While working in a mostly commercial arm of a mostly government contracting smallish business (http://radianinc.com/) in the mid-90s, the money people were not happy in the first few months of each year when there are so many Federal holidays, the lack of the "plus" while paying everyone's salaries pinched cash flow.
I also did a lot of non-classified Federal government fulfillment work in the '90s and early '00s and it wasn't radically different than the commercial world. More legal work was required, different sorts of sales processes in some cases, but e.g. at my first such job, when our "closer" salesman took me to e.g. NASA or a commercial firm to explain how we were going to fulfill our proposed commitment, there was essentially no difference. (State government contracting, and I'm sure the stupider Federal levels are a different matter, and to be avoided at all costs.)
I don't want to get started about cost-plus contracting, but here's a tip, if you're ever in that business again: hire friendly, personable, but not overly skilled people.
The government side is divided into two groups: program management, which are really only concerned with the money going out and are the other half of the contracting follies (see my DAU link previous), and project management; people who are on one hand interested in getting their work done and in the other on increasing the size and importance of their empires. Neither would know technical work from a hole in the ground, or if they did it was so long ago as to be irrelevant.
The project folks are on your side since the more there are of you, the more important they look. If your employees are good at being friendly with them, you're golden. All you have to do is convince the program management people that you're working really, really hard and that the problems are very, very difficult (hence the "not overly skilled" part), and the project managers will do most of that for you.
Just don't ever, ever, convert a cost-plus contract (where you as the prime contractor have cost-plus subcontracts) to fixed-price while not changing the subcontracts to fixed price. (And I'm looking at you, SAIC.)
There is one difference, in my experience between contracting commercially and for the government. The overhead for me when I was doing work for IBM (in the 90's and '00s) was 13-15%; the overhead for me doing work for NASA was somewhere close to 100%, judging by the GSA schedules for related contracts---I never could find the schedule for UNITeS or EAST.
Now Spark is introducing further safety features, and you're jumping on the bandwagon again to make sure that no one bothers to learn from it. Please stop.
If every CS101 student in the last 20 years had been taught to depend on, for example, bounded numeric types, verified pre and post conditions, and buffer and array overflow protection, the world would be a much better place. Let's try to not make the same mistakes (over and over) going forward.
All that, and the costly tools above the language and runtime, is a major reason I'm ignoring this ecosystem in favor of (tentatively) the seL4 one. Hmmm, and how close are Ada and SPARK to being supplied by a single source?
Also, FWIW, seL4 is not an ecosystem. It's a mish mash of Haskell prototype, Isabelle/HOL proofs, and C99 code put together by an extremely talented team. You might use some of their tricks, but there is no such thing as putting together an "seL4 ecosystem" software project.
Apart from the 100-odd tests of ACVC 1.11 that Ada/Ed failed, the major deficiency of the system is that, being an interpreter, it does not implement most representation clauses, and thus does not support systems programming close to the machine level.
So it sounds suitable for getting your feet wet, but not "industrial strength", and not useful for a lot of the things we want to do.
As for seL4's "ecosystem", well, it's certainly not polished like AdaCore's offerings (or so I assume, which for things like this is very iffy), but something I do believe I can clone, and seeing as I plan to start with a seL4 port, it qualifies for me.
You surely are aware that one of the reasons GCC became anything useful was the switch to paid SDKs on the UNIX world, which attracted developers not willing to pay for them?
And I most certainly remember that detail about GCC, having started playing that game no later than 1992 with Sun.
So, the empirical and anecdotal evidence contradicts your claim about Ada. It used specific design decisions to counter specific kinds of real-world issues they encountered. Now, your claims about DOD's big issues and how Ada cant solve those problems are spot on.
I'm not buying the old argument that it tries to do everything/too much therefore it's no-good, which seems to be the main thing people mention about Ada. A lot of languages tries to do a lot of things, and most of them let you chose what part of the language you use.
A few years back I was mainly doing C++, and looked a bit into Ada - it seems pretty alright. Not anything overly negative compared to the C++ work I was doing, and quite a few nifty things. Lacking is tooling and community though.
Does anyone know about the proposals that weren't selected?