[tjr]

I've worked on avionics flight management systems. We had reams of system requirements, multi-person code reviews for every line of code in the product, formal verification runs, system integration testing, field testing... The compilers used were qualified for our use. All libraries used were qualified. All operating system components used in the product were qualified. Internal tools that automated any part of the process were qualified.

I'm not sure what your criteria is for "mathematical" verification, but I see this sort of work as software engineering.

[jbondeson]

The aerospace and medical fields have done quite a bit to increase the rigor in building software, however there doesn't seem to be any push from them to codify their processes and establish some sort of push for the industry as a whole. The establishment of a true Software Engineering discipline would require some consensus on the use of formal methods in specification design, and then program verification.

The other hurdle is that you need the same rigor from your hardware designers. Just as structural engineers must rely on the rigor of steel manufacturers, we are held hostage by hardware manufacturers. Frankly the entire industry needs a wake up call.

As for formal verification, it is the mathematical proof (in the pure sense) that a program behaves exactly as speced -- the specification must also be formally verified for consistency. Currently this is only possible on relatively small programs, with the largest being several compiler back-ends being verified.

Here's a paper on what it took to formally verify the seL4 micro-kernel: http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf

[tjr]

Codify their processes?

http://en.wikipedia.org/wiki/DO-178B

On the avionics software I worked on, we (another group of people) designed and manufactured the hardware. I'm not as familiar with the process there, but I have no reason to believe that it wasn't done with similar rigor. [See http://en.wikipedia.org/wiki/DO-254]

I understand mathematical proof, but I wasn't sure that was what you meant. I did not realize that physical engineering projects are mathematically proven to that extent?

[jbondeson]

I'm sorry, I wasn't very precise in my language, I meant the industries working together to generate a more generic process that isn't tied to a specific industry. This would be done with the intention of building a Professional Software Engineer program.

Anything relying on the physical world obviously cannot be mathematically verified, however the mathematical rigor is still there in the modelling and testing.

[tjr]

Ah, I think I follow then. Mathematical proof of very large software systems may presently be impractical; the verification procedures currently in place for avionics systems are pretty daunting as they stand.

I'm not sure what we would gain from an overall software engineering professional qualification. While I am quick to point to avionics development as (in my opinion) being true software engineering, I also acknowledge that a great deal of software is not built using any methods even remotely as rigorous. But then, it also probably doesn't need to be.

You put a lot more rigor into building a house for people than you do a house for dogs, and you put a lot more rigor into building a skyscraper office building than you do a house. And rightly so. Each needs to withstand different levels of pressure. I see no reason to apply rigorous engineering processes to iPhone games; it would be a waste of time and resources.

As it is, the industries that require rigorous software development have produced their own standards. I suppose if you could ascertain the similarities across industries and codify that into general software engineering practices, that could be a good thing, but you'd probably still need industry-specific regulations to make sure nothing was missed.

I dunno. Maybe if more software needed extensive rigor it would be more obvious what needs to be done across industries.

[jbondeson]

There are tons of industries that should require it. The issue is that we focus in on the software that can directly kill us, rather than all the software that can indirectly do it. We instantly reason that all software we use to control things like cars or airplanes should be highly controlled, but what about financial software, phone systems, medical records software?

One of the sloppiest and haphazard programmers I ever worked with is now writing software for non-critical medical monitoring devices (external monitors like O2 sensors, and blood pressure monitors) and it scares the living daylights out of me. When I'm in a hospital room I look around to see if his company's hardware is in use. It might not kill me, but it could contribute to that end.

I'll come full circle around to my initial assertion that I don't know if we can even get to the point of a true Professional Software Engineer. Many of the tasks we deal with are highly abstract. How do we define an acceptable failure rate for a TCP stack? And even if we do, how do we take that into account for a monitoring application? There are many hard questions we have to tackle prior to our industry being taken seriously as a true engineering discipline.

What troubles me is that very few of the leaders in the software community even care about these questions.