Edsger Dijkstra famously derided software engineering as "how to program when you cannot".
But if being able to program means being able to write large programs and get them perfectly correct, then no one has ever been able to program, the great Prof. Dr. Dijkstra not excepted. We all have puny brains next to a million lines of code. That being the case, the study of "how to program when you cannot" is critical for those of us who actually need to write these large programs.
I like to say that software engineering is the art of managing complexity. Designing abstractions to be as general as possible, with interfaces as simple and clean as possible, and minimizing coupling, makes it much easier to think about how the major components of the system interact. And that's the key: if it's too hard to think about the system at a high level of abstraction, because the interfaces have too many special cases in them, more mistakes will be made.
I don't think I can agree with the OP that formal verification is the only thing that can fairly be called software engineering. I do agree that the more verification we can figure out how to do, the better. But I would point out that well-designed abstractions are still important even when you're doing formal verification; indeed, possibly more so, because without them, the proofs get to be even more complicated and difficult than they need to be. It's really the same phenomenon: systems that are hard to think about are also hard to prove things about.
Designing abstractions to be as general as possible, with interfaces as simple and clean as possible, and minimizing coupling, makes it much easier to think about how the major components of the system interact.
I think this is a false statement. In fact I think you're confusing modularity with abstraction.
Abstraction hides complexity, and abstractions are leaky; how the whole behaves can be strongly influenced by behaviours that leak from the abstractions. It took a couple of goes, but eventually we realized that DCOM and CORBA were poor ways to design distributed applications.
Abstractions should be as general as necessary, where necessity is subject to judgement.
Make code too abstract, and people may not understand it because it's not concrete enough, full of indirections and compositions and factory-factories; make it too concrete, and people may not understand it because it's too complex.
Creating an abstraction to share some code may pay off if there's sufficient clients for the code and they all have a similar usage profile, but it may be a false economy if the clients are few or the usage varied.
Modularity isn't an unalloyed good either. Too many modules and you may write code that acts optimally in a local way, but suboptimally globally because it has no access or awareness of other modules' behaviour. Modules designed around an abstraction may be substituted, but designing for module replacement is more often than not over-engineering. It's strongly encouraged by modern OO testing approaches, but IMO it puts the cart before the horse.
I'd like more people to realize that abstractions represent unknowns, and that any given implementation needs to be tested in an engineering materials sense, to find out what its force limits are, how it reacts under scale and pressure, so people using the abstraction are not just thinking about the abstraction, they are considering the real thing they're dealing with as well. It saves a lot of time going down dead ends.
I think Rich Hickey's "Simple Made Easy" is a perfect example. He enumerates an intellectual toolbox and why it's useful. He admits "you may not end up here [using these tools] but there's no reason not to start here." There are clearly cognitive and technical benefits to arranging software in particular architectures. That seems like engineering to me. You can't make an ideal engine either; it depends on whether you're powering a car or an airplane. Solving domain specific problems through technical architecting is about a good a definition of engineering as you can get. Software certainly fits that definition.
Actually, it is thinking in general that is the art of managing complexity. Software engineering is no different from any other type of engineering, in that it is also the art of making reasonable compromises.
Calling the discipline Software "Engineering" was the worst thing that could be done, at least given the current state of the art. Because of that, people thought you should write software the way you build a bridge or a car. The waterfall method came out of that, and it took decades to realize and recover.
Software development is more reliant on discrete math (and more generally the ability to reason abstractly) than math that helps model the physical world. Hopefully, Professional Engineering bodies will one day realize this and will adapt their program accreditation criteria accordingly.
"Because of that, people thought you should write software the way you build a bridge or a car."
The reason people think that is because they have no idea how the engineering to build a bridge or a car is done.
Note, the term is Software ENGINEERING not Software Assembly or Software Construction. The engineering work necessary to design a bridge or car is actually not TOO dissimilar to designing anything else. You have requirements (often vague, conflicting and changing) and constraints and you have to trade things off against each other to come up with a workable design solution.
The construction is just the compilation. Or perhaps the final coding/debugging. Or a combination. In construction, tiny engineering issues are often resolved by the construction crew at the site. Sometimes with input from engineers, sometimes not.
The problem is that building software merges the engineering (design/architecture) with the construction (coding/debugging/compiling/installation) that requires a rather broad range of skills. Most people working on small teams have to jump back and forth between the big picture (more engineeringy) to the small details (more constructiony) and back.
Finally, software development is no longer a new thing. People have been doing it for a half century. There are many people in the field today who's parents wrote software. And a few who's grandparents did it. It's high time we stop trying to draw analogies to building bridges or designing cars. Software Engineering is its own discipline with its own unique challenges and dynamics. Better to just take it for what it is.
No the waterfall method was a misquote by a non-tech reading a report on iterative, software development. The misappropriation took a life of it's own for control-freak managers. Anyone wanting an example of where sensible people went with software engineering can look at Cleanroom from the 80's:
The results speak for themselves. A modern approach is Altran/Praxis Correct by Construction method getting nearly zero-defect software. Some provably correct in SPARK.
Today's work can add symbolic analysis (eg KLEE), assertion-driven test generation, languages like Haskell, certified compilers, and so on. What you're seeing in mainstream isn't software engineering. It exists, though, in s niche by academics and industry.
On the contrary, the worst thing was the abandoning of the sound engineering principles and the obligatory professional certification. Since then, the trade has been open to, and flooded by, know-nothing lazy half-wits who, should they find themselves in any other industry or medicine, would be immediately disqualified (or, rather, would not be admitted in the first place).
While I totally agree with you on the 'it's not engineering in the engineering kind of sense'-part, there's another interesting point a friend once brought up in conversation:
At least where I'm from, telling people what I do, I often get labeled as a 'computer person'. You know, kind of estranged from the real world and not good for anything practical (and mind you, after college I shed a lot of my admittedly nerdy past). Coining the term 'software engineer', with the word 'engineer' being something people can relate to and see it as a respectable profession, I think can help a bit in conveying that yes, what we do is a real and important job and no, we are not all geeks that totally like to be in their dark basements all day.
If you write software that needs discrete math, like probabilistic stuff or graphs, it will need discrete math. If you write software that is meant to simulate, like maybe even simulate real bridges, or video games, or generative art, non-photorealistic rendering, ... it will involve some of the math that helps model the physical world. It makes more sense to just learn a lot of things and apply the union of that to software, even ideas surrounding managing complexity in architecture (Notes on the Synthesis of Form?) and so on and expose that through oneself to "software" as a new universe where creations can exist; than to quibble about what's more important and what's not in a prescriptive way about what others want to and don't want to do. Of course, I'm doing the latter here. :) Such is the cycle.
Software crafting is very much like building a bridge back in the days before xrays were around to detect cracks in metal and before metallury and casting were very reliable - that was back in the 1800s when anything made of metal could and did fail at any time - including bridges - quite often catastrophically. A high percentage of bridges folded, over time. How do you "engineer" what you can't measure (such as whether a metal beam is fatally flawed by a large crack inside?) You don't. We're getting there slowly.
I don't know if it was the worst thing. I agree that it was unfortunate for the one reason you gave (waterfall), but there are other reasons that a new discipline(/profession) would want to emulate the practices of an older and more established discipline.
Another reason to choose "engineering" was to encourage software practitioners to incorporate some of the proven methods of traditional engineering. As an example, I've noticed recently that ethics training is an established part of an Engineer's education, but not so with Software "Engineers".
There is always room to improve, and I don't think ignoring the past, and justifying that ignorance by saying "but we're different" is necessarily the best way to achieve that improvement.
Planning assumes you know what you're building. Most of my career has involved dealing with others who aren't sure of what they want, and whom change their minds on a regular basis.
But then it wouldn’t be called “hacking”, and so wouldn’t pass as software development these days. Instead, let’s have no planing whatsoever, no design and no requirements, have minimal time for actual development, “hack” code together and see where bugs take us. Aka “scrum”, “agile” and whatnot.
"Whither Software Engineering?", discussed in the OP, sounds like an interesting historical piece about how long it took for mathematics to be integrated into engineering work. The author is John Allen, who wrote Anatomy of Lisp.
FSCQ is a really great example of a large system with proofs of correctness using extraction from Coq.
Another well known project is CompCert the certified C compiler [1]. Which has seen a fair amount of external testing and use in verification of GCC and Clang as a reference for checking invalid compiled semantics [2] (to say nothing of compiling programs).
The problem with this line of thinking is that a piece of software is ultimately built to solve a problem in our real, messy, uncertain world. There is no way to "prove" that an application served its intended purpose. As Fred Brooks wrote: "Even perfect program verification can only establish that a program meets its specification. […] Much of the essence of building a program is in fact the debugging of the specification."
Exactly by the time you could formally prove the application is correct, the market will have moved on to something different. Right now the combination of quick to develop and mostly correct seems to be more desirable to companies then slow to develop and formally correct. The success of languages like JavaScript and python show this.
So what would such a curriculum look like? I've tried diving into this a few times and it often feels like hurling yourself against a wall in hopes of picking up bricks. You actually do make progress after a time but it's difficult to determine the curriculum flow.
For me I think it started with reading a throwaway aside on "type verification" and wondering what the heck that was. After a bunch of wikipedia searching into different types of type calculus (not fun), I saw a reference on dependent types, which led me to Coq tutorials, and then, in an effort to be more practical, learning more Scala and a some Haskell - reasoning being that even if they didn't have full support for dependent types, at least their type systems were on the right track.
Failed efforts so far have been learning TLA+ and Idris (I haven't yet found a way to apply any learning), and trying to get through some youtube lectures on homotopic type theory. Maybe next time.
There exists a body of theory about how to do software engineering as described here, but there doesn't exist a sizable community of software engineers willing to do this kind of work on a reasonably large scale. Judging by HN (which itself probably represents the upper-end of 'engaged' software developers), most people fidget uncomfortably when forced to explicitly declare derived types, and gnash their teeth when faced with Haskell monads; who among you would make a career out of writing Coq proofs about system correctness?
Optimistically, the community might come around to realizing that this sort of development is at least desirable, and we might wind up with the basic components of popular OSes, or of firmware for dangerous things like cars and medical devices, being produced via provably-correct processes. But that will almost certainly wholly exhaust humanity's reserves of strongly math-educated software engineers (not to mention, industry's willingness to pay for it.) Software engineering may be impossible because most humans don't like math.
> there doesn't exist a sizable community of software engineers willing to do this kind of work on a reasonably large scale
also on the other side there's a very limited pool of employers willing to pay for this kind of engineering - aereospace and military mostly, and the second is cheapening out too.
I think a significant issue in software is the comparatively unconstrained input space.
I would imagine the average natural gas power plant would have more than a few issues if you fed it pure hydrogen instead of whatever methane based mixture it was designed for. Similarly I imagine there are other inputs that have tight specification, lubricants, etc. But, these inputs are relatively easy to control via both human and machine processes and there aren't that many combinations you would consider valid. There are complex inputs in the physical world, for example the impact of complex wind patterns on bridges, but I still feel this is simpler than many input spaces in software.
In software, at some level you're almost always dealing with human or machine generated input which may be very complex in nature such that that even after all reasonable efforts at validation the size of the possible input space is massive if not effectively infinite. We're getting a bit better at dealing with this, e.g. fuzzing, but there is a long way to go for fuzzing to be viable on more complicated inputs.
Computer Science is a science field, therefore computer scientists usually see themselves as something more than an engineer - you don't want to apply the same knowledge over and over to make something exactly as the known knowledge tells you to do, you want to try new things and experiment with new ideas. That's the general mentality of the degree by itself.
Real "software engineering" would have to be done with Agda, Coq, or similarly tools - theorem provers that guarantee your solution is sound. It is done that way for software that absolutely cannot fail (eg, aerospatial). Unfortunately, engineers are usually too far away from this kind of knowledge - and sometimes even doubt this is possible or doable, even if you direct them to the research (!).
By the way, software engineering disciplines are usually depressive OO garbage, frameworks and all that non-sense that comes with excessive Java usage, and frankly never teach anything about reliability or even proving programs correct - which should have been their primary goal.
When you build a bridge, a power station, or a wind turbine, you're creating something of known economic value for several decades, even centuries. The whole process is expected to have little to no business deliverables for years. That lends physical engineering nicely to an established set of standards. In software, we're often innovating entirely new products, and people want to see working proofs of concept, and see organic growth with the user base without getting locked in to preexisting concepts of what the product should do the business figures out what the market is.
The nexus in products like vehicular and medical equipment software might be a good place to start implementing something like a discipline, but those systems are so much more singular and simplistic in their product function (not the implementation, I realize) than what the average software dev is working on that I don't even know how much downstream influence it would have.
Nice title, although I don't think the proposed solution (formal proof methods) is the answer. My own view is that building software is more of a design process than an engineering process, for the simple reason that software rarely has the kind of fixed requirements that make engineering solutions possible. Most software is constantly evolving and the factors that make it possible to evolve well include things like conceptual clarity and modularity, about which formal methods have nothing to say.
There was a movement around 20 years ago to establish a field of practice called"software design" but I don't think it went anywhere. The problems remain the same though. http://hci.stanford.edu/publications/bds/
There is a movement going on from weak typing back to strong typing which is the same idea approached from the opposite (practical) end. Have the computer do more work to verify program correctness by rejecting invalid expressions.
I never got the excitement that some of my college classmates had for JavaScript because they didn't have to 'deal with types'. I always much preferred a compiler telling me that this won't work instead of having to find some obscure type bug at runtime. Don't get me wrong, I still very much liked programming in JavaScript for other merits, especially the functional aspect or flexibility of extending your program simply in a browser command line window.
EDIT: I kind of got distracted by my JavaScript-story here. What I originally wanted to post was:
I always had an interest in philosophy and the logical thinking you can apply in software development (i.e. you can save yourself so much trouble by just thinking through your system thoroughly before writing even one line of code). However, the general sentinment that I also got from a lot of my classmates was that they didn't want have anything to do 'with any of this stuff' (this stuff being the humanities) but didn't have a problem with cracking hard math problems day in day out (which for me at least is pretty similar to using logical thinking / philosophy on a less abstract level).
Sorry, if by my large edit I confused some people!
To some extent, they have. The big breakthrough was "auto" in C++. (I wanted to call it "let", but that involved introducing a new keyword.) The type of a local variable in C++ is quite verbose for iterators. This discouraged the use of iterators in FOR statements. With "auto", you can write
for (auto p = thing.begin(); p != thing.end(); p++) { ... }
for anything that uses an iterator. No need to write out the whole iterator declaration for p. Or to generate it in a template. Suddenly, iterators became far easier to use.
Since then, Go and Rust have taken a similar approach of limited type inference. There seems to be a developing consensus that function parameters should have explicitly declared types, but within a function, type information should be inferred when possible.
We're seeing convergence from the other direction, with Python and Javascript (via add-ons such as TypeScript) acquiring type declarations.
For me the biggest advantage of strong typing is ide quality that follows - refactoring support ans code completion are much much better for example. Makes work on larger project significantly easier.
Teams that are 100% invested on having clean, tested and reliable code can have software engineering, absolutely.
The problem is that outside of the tech industry, most of the people with the pursestrings don't see the value in it most of the time.
Why? When their main widget makes $100M/month (for example) and its current maintenance, as fucked as it might be, is ($1-10M/month, or 1-10% of revenue), spending, say, $1-10M to drop that OpEx to half of current costs, prima facie, doesn't make a lot of sense.
What changes that equation is when some event that could have been prevented by good software engineering principles occurs. Good examples: the latest British Airways IT meltdown, LinkedIn's massive data breach, 100's of millions of CC's stolen from TJ Maxx and others.
You see, when something happens that threatens that $100M/month cash machine, many millions of dollars of bonuses, raises, hirings, parties, expansion plans, and other general symbols of growth and progress get threatened as well. THAT is what people with the pursestrings don't want to see messed with.
The overall problem with this is that it's reactionary, and every reactive event has a lifespan. So it takes finding someone with connections that can either capitalize on an unfortunate event trailblazing a path for software engineering to happen, or tell a good enough story of previous woes and misfortunes that can make that happen all the same.
TL;DR: If you want "software engineering" to happen at your company, you need to tell a compelling story of how NOT making it happen will lead to great losses, and then you need to be extremely patient.
I've looked into Coq and like a lot of others here tried to learn the theory and application but it is so far removed from my daily work that the benefits are basically non-existent. I've gotten way more mileage out of trying to learn systems theory and cybernetics than anything related to dependent types.
People think this is a tool problem but it's not. Well, the tools kinda suck but fundamentally it comes down to culture and mind share. My background is in pure math but my programming knowledge is steeped in the hacker tradition. It is very hard to overcome all that momentum.
There is no killer application for verified programming. Whatever you can do in Coq in 10 weeks you can do in C in 2 weeks with a few extra buffer overflows. We'd be further ahead if there were more tools for validating C code than trying to rewrite the world with dependent types.
There’s a terrible trend in the San Francisco tech scene where “engineer” is viewed as a synonym for “software engineer”, which is itself a synonym for “programming”. It isn’t.
That said, I tend to disagree with people who believe the solution is "use Coq".
We have existence proofs that Software Engineering is possible. For example, look at what NASA did with the Space Shuttle flight control software. But for most business domains, real engineering simply isn't cost effective.
I'd like to contribute a definition of the words "engineer" and "engineering" from an old dictionary I had lying around.
From Webster's (1948):
engineer: n. 1. [Rare], a person who makes engines. 2. a person skilled or occupied in some branch of engineering: as, a mechanical engineer, an electrical engineer. 3. the operator of an engine; especially the driver of a railroad locomotive. 4. in military science, a member of that branch of the army which is concerned with the construction and demolition of bridges, roads, and fortifications, the laying and sapping of mines, etc. Abbreviated E., e., eng., engin., engr. v.t. 1. to plan, construct, or manage as an engineer; hence, 2. to contrive; manage skillfully; superintend; guide (a measure, action, etc. through).
engineering: n. 1. the planning, designing, construction, or management of machinery, roads, bridges, buildings, fortifications, waterways, etc.; science, profession, or work of an engineer: abbreviated E., e., eng., egin. 2. a maneuvering or managing.
Feels like some stability in computing generations (CPU/GPU) or interaction paradigms (mobile) will be necessary to formalize software engineering. Until bridges/etc had a relative standard building each one was a craft. Not to say there hasn't been generational tech in traditional engineering, but generally not on the order of every few years.
[+] [-] ScottBurson|8 years ago|reply
But if being able to program means being able to write large programs and get them perfectly correct, then no one has ever been able to program, the great Prof. Dr. Dijkstra not excepted. We all have puny brains next to a million lines of code. That being the case, the study of "how to program when you cannot" is critical for those of us who actually need to write these large programs.
I like to say that software engineering is the art of managing complexity. Designing abstractions to be as general as possible, with interfaces as simple and clean as possible, and minimizing coupling, makes it much easier to think about how the major components of the system interact. And that's the key: if it's too hard to think about the system at a high level of abstraction, because the interfaces have too many special cases in them, more mistakes will be made.
I don't think I can agree with the OP that formal verification is the only thing that can fairly be called software engineering. I do agree that the more verification we can figure out how to do, the better. But I would point out that well-designed abstractions are still important even when you're doing formal verification; indeed, possibly more so, because without them, the proofs get to be even more complicated and difficult than they need to be. It's really the same phenomenon: systems that are hard to think about are also hard to prove things about.
[+] [-] barrkel|8 years ago|reply
I think this is a false statement. In fact I think you're confusing modularity with abstraction.
Abstraction hides complexity, and abstractions are leaky; how the whole behaves can be strongly influenced by behaviours that leak from the abstractions. It took a couple of goes, but eventually we realized that DCOM and CORBA were poor ways to design distributed applications.
Abstractions should be as general as necessary, where necessity is subject to judgement.
Make code too abstract, and people may not understand it because it's not concrete enough, full of indirections and compositions and factory-factories; make it too concrete, and people may not understand it because it's too complex.
Creating an abstraction to share some code may pay off if there's sufficient clients for the code and they all have a similar usage profile, but it may be a false economy if the clients are few or the usage varied.
Modularity isn't an unalloyed good either. Too many modules and you may write code that acts optimally in a local way, but suboptimally globally because it has no access or awareness of other modules' behaviour. Modules designed around an abstraction may be substituted, but designing for module replacement is more often than not over-engineering. It's strongly encouraged by modern OO testing approaches, but IMO it puts the cart before the horse.
I'd like more people to realize that abstractions represent unknowns, and that any given implementation needs to be tested in an engineering materials sense, to find out what its force limits are, how it reacts under scale and pressure, so people using the abstraction are not just thinking about the abstraction, they are considering the real thing they're dealing with as well. It saves a lot of time going down dead ends.
[+] [-] ellius|8 years ago|reply
[+] [-] 801699|8 years ago|reply
What does it mean when someone is only able (or only wants) to write small programs?
For example, small programs that can work together to form a "system" for managing something.
Is that not considered "software engineering"? If not, what is it called?
(Embedded software engineering? But not all small software is "embedded".)
What has a better chance of being error-free, a small program or a large one?
Should "ability to program" be measured by how large a program one can write?
For example, if someone writes a small UNIX utility, but does not write a large program, should we assume he does not know how to program?
[+] [-] Koshkin|8 years ago|reply
[+] [-] haskellandchill|8 years ago|reply
[+] [-] esfandia|8 years ago|reply
Software development is more reliant on discrete math (and more generally the ability to reason abstractly) than math that helps model the physical world. Hopefully, Professional Engineering bodies will one day realize this and will adapt their program accreditation criteria accordingly.
[+] [-] rmah|8 years ago|reply
The reason people think that is because they have no idea how the engineering to build a bridge or a car is done.
Note, the term is Software ENGINEERING not Software Assembly or Software Construction. The engineering work necessary to design a bridge or car is actually not TOO dissimilar to designing anything else. You have requirements (often vague, conflicting and changing) and constraints and you have to trade things off against each other to come up with a workable design solution.
The construction is just the compilation. Or perhaps the final coding/debugging. Or a combination. In construction, tiny engineering issues are often resolved by the construction crew at the site. Sometimes with input from engineers, sometimes not.
The problem is that building software merges the engineering (design/architecture) with the construction (coding/debugging/compiling/installation) that requires a rather broad range of skills. Most people working on small teams have to jump back and forth between the big picture (more engineeringy) to the small details (more constructiony) and back.
Finally, software development is no longer a new thing. People have been doing it for a half century. There are many people in the field today who's parents wrote software. And a few who's grandparents did it. It's high time we stop trying to draw analogies to building bridges or designing cars. Software Engineering is its own discipline with its own unique challenges and dynamics. Better to just take it for what it is.
[+] [-] nickpsecurity|8 years ago|reply
http://infohost.nmt.edu/~al/cseet-paper.html
The results speak for themselves. A modern approach is Altran/Praxis Correct by Construction method getting nearly zero-defect software. Some provably correct in SPARK.
http://www.anthonyhall.org/c_by_c_secure_system.pdf
Today's work can add symbolic analysis (eg KLEE), assertion-driven test generation, languages like Haskell, certified compilers, and so on. What you're seeing in mainstream isn't software engineering. It exists, though, in s niche by academics and industry.
[+] [-] Koshkin|8 years ago|reply
On the contrary, the worst thing was the abandoning of the sound engineering principles and the obligatory professional certification. Since then, the trade has been open to, and flooded by, know-nothing lazy half-wits who, should they find themselves in any other industry or medicine, would be immediately disqualified (or, rather, would not be admitted in the first place).
[+] [-] Joe-Z|8 years ago|reply
At least where I'm from, telling people what I do, I often get labeled as a 'computer person'. You know, kind of estranged from the real world and not good for anything practical (and mind you, after college I shed a lot of my admittedly nerdy past). Coining the term 'software engineer', with the word 'engineer' being something people can relate to and see it as a respectable profession, I think can help a bit in conveying that yes, what we do is a real and important job and no, we are not all geeks that totally like to be in their dark basements all day.
[+] [-] nikki93|8 years ago|reply
[+] [-] Nomentatus|8 years ago|reply
[+] [-] Avshalom|8 years ago|reply
Seeing as the 'recovery' seems to be largely move fast, break things, worry about security never. I'd rather software not have recovered.
[+] [-] pjmlp|8 years ago|reply
Now that the agile wave has come and gone, we are doing sprint waterfalls.
[+] [-] ebcode|8 years ago|reply
Another reason to choose "engineering" was to encourage software practitioners to incorporate some of the proven methods of traditional engineering. As an example, I've noticed recently that ethics training is an established part of an Engineer's education, but not so with Software "Engineers".
There is always room to improve, and I don't think ignoring the past, and justifying that ignorance by saying "but we're different" is necessarily the best way to achieve that improvement.
[+] [-] exabrial|8 years ago|reply
[+] [-] jameslk|8 years ago|reply
See also: Big Ball of Mud http://www.laputan.org/mud/
[+] [-] LeoNatan25|8 years ago|reply
[+] [-] ScottBurson|8 years ago|reply
Sometimes nothing slows you down as much as being in too much of a hurry.
[+] [-] unknown|8 years ago|reply
[deleted]
[+] [-] Joe-Z|8 years ago|reply
[+] [-] Too|8 years ago|reply
[+] [-] cordite|8 years ago|reply
[+] [-] unknown|8 years ago|reply
[deleted]
[+] [-] dang|8 years ago|reply
Can anyone find that paper online? https://news.ycombinator.com/item?id=962733 points to a blog post about it from 2009, but none of the links seem to work.
[+] [-] johnbender|8 years ago|reply
Another well known project is CompCert the certified C compiler [1]. Which has seen a fair amount of external testing and use in verification of GCC and Clang as a reference for checking invalid compiled semantics [2] (to say nothing of compiling programs).
1 http://compcert.inria.fr
2 https://blog.regehr.org/archives/1052
[+] [-] protonfish|8 years ago|reply
[+] [-] donovanm|8 years ago|reply
[+] [-] tunesmith|8 years ago|reply
For me I think it started with reading a throwaway aside on "type verification" and wondering what the heck that was. After a bunch of wikipedia searching into different types of type calculus (not fun), I saw a reference on dependent types, which led me to Coq tutorials, and then, in an effort to be more practical, learning more Scala and a some Haskell - reasoning being that even if they didn't have full support for dependent types, at least their type systems were on the right track.
Failed efforts so far have been learning TLA+ and Idris (I haven't yet found a way to apply any learning), and trying to get through some youtube lectures on homotopic type theory. Maybe next time.
[+] [-] maxander|8 years ago|reply
Optimistically, the community might come around to realizing that this sort of development is at least desirable, and we might wind up with the basic components of popular OSes, or of firmware for dangerous things like cars and medical devices, being produced via provably-correct processes. But that will almost certainly wholly exhaust humanity's reserves of strongly math-educated software engineers (not to mention, industry's willingness to pay for it.) Software engineering may be impossible because most humans don't like math.
[+] [-] LoSboccacc|8 years ago|reply
also on the other side there's a very limited pool of employers willing to pay for this kind of engineering - aereospace and military mostly, and the second is cheapening out too.
[+] [-] haskellandchill|8 years ago|reply
[+] [-] mbell|8 years ago|reply
I would imagine the average natural gas power plant would have more than a few issues if you fed it pure hydrogen instead of whatever methane based mixture it was designed for. Similarly I imagine there are other inputs that have tight specification, lubricants, etc. But, these inputs are relatively easy to control via both human and machine processes and there aren't that many combinations you would consider valid. There are complex inputs in the physical world, for example the impact of complex wind patterns on bridges, but I still feel this is simpler than many input spaces in software.
In software, at some level you're almost always dealing with human or machine generated input which may be very complex in nature such that that even after all reasonable efforts at validation the size of the possible input space is massive if not effectively infinite. We're getting a bit better at dealing with this, e.g. fuzzing, but there is a long way to go for fuzzing to be viable on more complicated inputs.
[+] [-] leovonl|8 years ago|reply
Real "software engineering" would have to be done with Agda, Coq, or similarly tools - theorem provers that guarantee your solution is sound. It is done that way for software that absolutely cannot fail (eg, aerospatial). Unfortunately, engineers are usually too far away from this kind of knowledge - and sometimes even doubt this is possible or doable, even if you direct them to the research (!).
By the way, software engineering disciplines are usually depressive OO garbage, frameworks and all that non-sense that comes with excessive Java usage, and frankly never teach anything about reliability or even proving programs correct - which should have been their primary goal.
[+] [-] pjmlp|8 years ago|reply
[+] [-] lr4444lr|8 years ago|reply
The nexus in products like vehicular and medical equipment software might be a good place to start implementing something like a discipline, but those systems are so much more singular and simplistic in their product function (not the implementation, I realize) than what the average software dev is working on that I don't even know how much downstream influence it would have.
[+] [-] wbl|8 years ago|reply
[+] [-] mtraven|8 years ago|reply
There was a movement around 20 years ago to establish a field of practice called"software design" but I don't think it went anywhere. The problems remain the same though. http://hci.stanford.edu/publications/bds/
[+] [-] Joeri|8 years ago|reply
Maybe the two will meet at some point?
[+] [-] Joe-Z|8 years ago|reply
EDIT: I kind of got distracted by my JavaScript-story here. What I originally wanted to post was: I always had an interest in philosophy and the logical thinking you can apply in software development (i.e. you can save yourself so much trouble by just thinking through your system thoroughly before writing even one line of code). However, the general sentinment that I also got from a lot of my classmates was that they didn't want have anything to do 'with any of this stuff' (this stuff being the humanities) but didn't have a problem with cracking hard math problems day in day out (which for me at least is pretty similar to using logical thinking / philosophy on a less abstract level).
Sorry, if by my large edit I confused some people!
[+] [-] Animats|8 years ago|reply
Since then, Go and Rust have taken a similar approach of limited type inference. There seems to be a developing consensus that function parameters should have explicitly declared types, but within a function, type information should be inferred when possible.
We're seeing convergence from the other direction, with Python and Javascript (via add-ons such as TypeScript) acquiring type declarations.
So the two are meeting.
[+] [-] watwut|8 years ago|reply
[+] [-] nunez|8 years ago|reply
The problem is that outside of the tech industry, most of the people with the pursestrings don't see the value in it most of the time.
Why? When their main widget makes $100M/month (for example) and its current maintenance, as fucked as it might be, is ($1-10M/month, or 1-10% of revenue), spending, say, $1-10M to drop that OpEx to half of current costs, prima facie, doesn't make a lot of sense.
What changes that equation is when some event that could have been prevented by good software engineering principles occurs. Good examples: the latest British Airways IT meltdown, LinkedIn's massive data breach, 100's of millions of CC's stolen from TJ Maxx and others.
You see, when something happens that threatens that $100M/month cash machine, many millions of dollars of bonuses, raises, hirings, parties, expansion plans, and other general symbols of growth and progress get threatened as well. THAT is what people with the pursestrings don't want to see messed with.
The overall problem with this is that it's reactionary, and every reactive event has a lifespan. So it takes finding someone with connections that can either capitalize on an unfortunate event trailblazing a path for software engineering to happen, or tell a good enough story of previous woes and misfortunes that can make that happen all the same.
TL;DR: If you want "software engineering" to happen at your company, you need to tell a compelling story of how NOT making it happen will lead to great losses, and then you need to be extremely patient.
[+] [-] dkarapetyan|8 years ago|reply
People think this is a tool problem but it's not. Well, the tools kinda suck but fundamentally it comes down to culture and mind share. My background is in pure math but my programming knowledge is steeped in the hacker tradition. It is very hard to overcome all that momentum.
There is no killer application for verified programming. Whatever you can do in Coq in 10 weeks you can do in C in 2 weeks with a few extra buffer overflows. We'd be further ahead if there were more tools for validating C code than trying to rewrite the world with dependent types.
[+] [-] powera|8 years ago|reply
That said, I tend to disagree with people who believe the solution is "use Coq".
[+] [-] nradov|8 years ago|reply
https://www.fastcompany.com/28121/they-write-right-stuff
[+] [-] ebcode|8 years ago|reply
From Webster's (1948):
engineer: n. 1. [Rare], a person who makes engines. 2. a person skilled or occupied in some branch of engineering: as, a mechanical engineer, an electrical engineer. 3. the operator of an engine; especially the driver of a railroad locomotive. 4. in military science, a member of that branch of the army which is concerned with the construction and demolition of bridges, roads, and fortifications, the laying and sapping of mines, etc. Abbreviated E., e., eng., engin., engr. v.t. 1. to plan, construct, or manage as an engineer; hence, 2. to contrive; manage skillfully; superintend; guide (a measure, action, etc. through).
engineering: n. 1. the planning, designing, construction, or management of machinery, roads, bridges, buildings, fortifications, waterways, etc.; science, profession, or work of an engineer: abbreviated E., e., eng., egin. 2. a maneuvering or managing.
[+] [-] unknown|8 years ago|reply
[deleted]
[+] [-] millisecond|8 years ago|reply