I vigorously contest the idea that software engineering cannot be rigorous and so shouldn't try.
There are six thousand types of programs (as a wild guess), and they all interact with each other in an exponential explosion of complexity.
For a formal method to work, it has to be generally applicable across a wide range of situations. There are methods like that in software engineering, and you see them in situations where the program is potentially life-threatening. But most programs would be hindered by this rigor.
When programming in a well-typed language, everything we do is a degenerate proof of something. I think it's entirely reasonable to try and make it easier to make less degenerate proofs, and encourage the re-centering of proofs as the atomic unit in programming, because they are for programming (as in math) a well-defined, solid formal system that solid systems can be built on in a way that nothing else can be in software, at least thus far.
In a world where software flows more freely than water, the correctness and reliability of software systems must be taken with utmost seriousness. This applies to basically any tool that contacts end users, and a lot of ones that don't as well.
What do you propose as the theoretical basis for the engineering science of software development?
It's also self-evident that in most situations, correctness and reliability aren't a concern. The counterexamples account for maybe 1% of the field. 99% of the time, if your program breaks, you can pay someone to go fix it and no serious harm was done. Even Github outages, which affect almost all of us, hardly matter.
Yes. Writing software is not math. Does it use math concepts? Of course, but so does just about everything else. While we're at it, writing software is also not engineering, even though there are engineering concepts that can be applied.
Writing software is its own thing. Pretending that it's something else (like math or engineering) invariably leads to category errors.
Think about food recipes. They certainly use measurements and timing, and engineering principles can certainly be applied (especially when executing them on an industrial scale) but they are not math (or engineering) either. Examining the measurements, timing, and the production chain doesn't tell you anything about whether the recipe is delicious or inedible.
Arguing that a piece of software should be "proven correct" makes about as much sense as arguing that a recipe should be "proven correct". You might as well judge the recipe by the standards of poetry ("Does it have evocative imagery? Does it rhyme or alliterate well?").
People have been chasing the unicorn of software correctness proofs for 60 years, with a notable lack of generalizable success (there are plenty of toy examples, of course). What usually happens is that the "programming is math" people come up with some bizarre academic language that no real-world programmer would use unless forced to do so at gunpoint (followed by the new language sinking without a trace). Alternatively, the "programming is engineering" people come up with some baroque formal process that requires you to write a 500 page document and get six committees to sign off on it before you can write "Hello, world". I'm old enough that I've seen these things happen multiple times.
>It's also self-evident that in most situations, correctness and reliability aren't a concern.
I wouldn't say they aren't a concern at all, but if you're wasting six months screwing around with formal proofs, UML diagrams, or things of that nature, while in the meantime your competitor is iterating three or four times, that is definitely a concern. Operate that way and your milkshake is going to be drunk, yo.
You're wrong, and I've explained this upthread.
>Think about food recipes.
Do you have experience with non-imperative programming paradigms? I'm sorry to say that the comparison to recipes in this context seems fairly naive.
>People have been chasing the unicorn of software correctness proofs for 60 years, with a notable lack of generalizable success (there are plenty of toy examples, of course).
Static type systems are arguably a product of this, especially advanced ones like Haskell's.
>What usually happens is that the "programming is math" people come up with some bizarre academic language that no real-world programmer would use unless forced to do so at gunpoint (followed by the new language sinking without a trace).
Now you're just being anti-intellectual. The whole point is that the real-world programmers are stumbling into all this crap constantly without realizing it. It's completely fucking unavoidable and very much tied up with the fact that programming is math. The only question is what you choose to do about that: learn the math, or stay ignorant.
I don't mean to be condescending but I find comparing UML diagrams and proof assistants a little offensive (among other things), and it suggests you don't know what you're talking about. Modern proof assistants and other formal techniques like dependent typing happen while you're programming (Idris/Agda) or generate programs themselves (Coq), they aren't some sort of Waterfall-ish thing where you have to deal with all the ceremony before you start to get shit done. On the contrary, you get shit done, and it works better when you're done with it too.
That aside, there seems to be something missing in your analysis, or there would be a lot of successful startups stealing the market using proof assistants and formal techniques. It's not anti intellectual to point out that programmers don't want to use academic languages that have poor usability, steep learning curves, and garbage for standard libraries.
Consider when a regular house is being built. There are many problems that could be avoided if an engineering firm spent an entire year analyzing the designs and their interactions with the target site. However, that's not done because it takes significantly longer and costs obscene amounts of money.
It's easier for the construction crew to fix problems as they encounter them and for the owner to do repairs on the house 40 years later. Yeah, the house isn't as reliable, but it cost 100,000 instead of 1,000,000.
If you want developers and managers on your side, you need to show them benefits over the quick development of python/php/Javascript other than bugs in edge cases being less frequent. Don't just bemoan how unenlightened everyone is.
However, it's worth pointing out that you don't magically get the final program out of the TLA proof. The proof only works for the abstraction level that you chose to write it at.
There is also a certain level of compromise. By relaxing the requirements a tad, you can still gain many of the benefits while maintaining the light and nimble feel.
So why don't startups use this? Well because there are entrenched technologies that make it very difficult that have nothing to do with the merits of the approach itself.
It is up to us, as developers to take the charge and push for these techniques through open source development, advocacy, and training.
But to claim these techniques are a failure simply because startups aren't using them is pretty ridiculous.
I've never seen that used in the wild (though I'm in the wrong domain (web) these days).
> You're wrong, and I've explained this upthread.
I suspect there is a difference in semantics, here. Software is inherently mathematical, yes. But the practice of writing software is not the practice of doing math.
The output of doing math is proofs. The output of writing software is...something that does something when run on a computer, hopefully interesting, meaningful, useful, or entertaining. In the vast majority of cases, we have not and will not need formal proofs of correctness for software to achieve these things.
If I want a blur effect on some portion of a UI, and choose to implement that with a Gaussian blur, what value is there in formally proving that a specifically Gaussian blur has been applied? All of this is inherently mathematical, but that doesn't imply a need for mathematical proof.
Here I also thing that 'Turing_Machine is both wrong in details and correct in the general point with their recipe example:
> Examining the measurements, timing, and the production chain doesn't tell you anything about whether the recipe is delicious or inedible.
You could, in principle, apply the knowledge of medicine, chemistry and biology, coupled with process engineering and wide-scale people studies, to construct a theory of tasty foods, which could lead to the situation in which you could evaluate any recipe on a theoretical basis. But getting to that state would require tons of up-front work to be done (some of which is being done for unrelated reasons, so maybe in the future a "food theory" will assemble itself) - and in the meantime, getting a piece of tasty food is done much faster and cheaper by finding the solution instead of deriving it. This search is done through iteration.
Similarly, in software, 99% of the time we find a solution, not derive it from first principles - because the former is much cheaper when we care about the solution, and not solving the entire general class of a problem at the same time.
The reason for all the confusion is that programmers are already doing math. They just don't realize it and reinvent the wheels invented by the math community in the past century. It's a matter of semiotics.
Some aspects of language design are reinventing wheels invented by the math community. This is far from constituting the set of "writing software" or "software engineering".
But assuming you're right, I'd like to know - what mathematical wheels am I reinventing in my dayjob of building UIs that let people click up some stuff that later gets put in business-specific XMLs?
The XML as a vessel of human-knowledge is limited. Good intentions have brought it OWL/RDF, XML Schema, XSLT; examples where others before us have tried to extend the XML into the domain of semantics and algorithms. Nevertheless, it was found that, without an expressive type system, large and complex business domains cannot be modeled. Apparently, in order to model abstract business domains, we need a language that composes both high- and low-level with near invisible seams.
So, that click-your-XML-application might benefit from a reflective logic, enabling the user to explore the possible state-spaces. If your app uses relational algebra from DBMSs, it might be able to combine the relational algebra with the algebra defined by your schema's. The UI state-space and the XML schema might be an isomorphism, which helps prove completeness of your UI-builder implementation.
Above all, the mathematical way of thinking helps reasoning, communication and correctness. It might not be the only way or perhaps the way is dated. Nevertheless, ignoring math as a programmer, feels like ignoring music theory as a musician or linear algebra as a structural engineer.
> ignoring math as a programmer, feels like ignoring music theory as a musician or linear algebra as a structural engineer.
We're not ignoring math.
It's like you read the article, and set about disproving it, without ever really understanding it.
No. I'm not.
Are formal math and engineering useful in cooking food? Yes, they can be (particularly if executing on an industrial scale). Are they necessary? Not really. Plenty of great cooks just throw in ingredients in the amounts that seem right to them, perhaps tasting the result once in a while. Are they sufficient? Nope. If the best mathematician and best engineer in the world collaborated, the result might be edible or it might be an inedible mess.
If neither formal math and engineering are necessary nor sufficient to produce good cooking, we can safely conclude that cooking is not math or engineering.
> Static type systems are arguably a product of this, especially advanced ones like Haskell's.
Haskell is used by, to a first approximation, no one. Which was my point.
> Now you're just being anti-intellectual.
No, I'm not.
> The only question is what you choose to do about that: learn the math, or stay ignorant.
I was one math class away from getting a dual BS in math and CS in undergrad. Rather than stick around for another semester, I took the BSCS and went to grad school.
You can safely assume that I "learned the math", and that I am not "anti-intellectual".
The point here is that while, on the most fundamental level, the universe may indeed be made of math, that doesn't mean that treating everything with the math toolbox is the best way to proceed. Expecting that math methods will produce great software is a fundamentally goofy idea -- just as it would be to expect math to produce great poetry, painting, architecture, or anything else (and the same for engineering).
Bingo. Good thing we're talking about programming, and not cooking.
I asked if you understood what you were saying because you can't really cook declaratively, recipes are inherently imperative. The comparison to programming thus only fits for imperative languages.
>Haskell is used by, to a first approximation, no one. Which was my point.
If that's your point, then I agree. Not sure how that's in disagreement with my points though.
>No, I'm not.
So what then were you intending to convey by vague references to incomprehensible academia? Surely you weren't meaning to imply they're just wrong, were you?
>The point here is that while, on the most fundamental level, the universe may indeed be made of math, that doesn't mean that treating everything with the math toolbox is the best way to proceed.
Yes, but such a general claim is not what I'm arguing for.
>Expecting that math methods will produce great software is a fundamentally goofy idea -- just as it would be to expect math to produce great poetry, painting, architecture, or anything else (and the same for engineering).
Well, it of course depends on what you mean by "great" software. But I still think you're missing the point here. Computer science is a lot closer to math than poetry, painting, and architecture are. There is a direct, elegant, simple, formal correspondence between programs and proofs. The same cannot be said for those other disciplines.
My only claim is that proofs are slightly more solid intellectually and formally speaking than programs, so converting more programs into proofs will make easier to reason about, and since programs can be easily converted into proofs (relative to poems or architecture or paintings or whatever) that this is probably a good idea. I still don't understand what your objection to that claim is.
I am not comparing recipes directly to programming. I used recipes as an example of something that has mathy and engineery facets, but that is not engineering or math.
> So what then were you intending to convey by vague references to incomprehensible academia?
I wasn't making "vague references" to anything, nor did I say that academic languages were "incomprehensible". I did say they were bizarre, which is a different thing entirely.
I'm not sure why you find it hard to believe that someone could understand academic languages of the sort you evidently prefer, and yet somehow still choose not to use them. Your attitude seems to be that anyone who doesn't use your preferred methods is "anti-intellectual", "ignorant", or any of the various other personal insults you've used.
Why not just go off and write some awesome software using your methods? If they work as well as you claim, you'll have some hard evidence to back up your assertions
>There is a direct, elegant, simple, formal correspondence between programs and proofs."
You are defining great software as "software that can be proved to behave in accordance with some formal spec", while people who actually use software (i.e., the people who pay the bills) define great software as software that performs the task they need to have done, can be written economically, and that is easy to use.
By your definition, a great recipe would be one that came out exactly the same every time, even if it tasted like shite, or took three weeks to make, or...
> If that's your point, then I agree.
You are agreeing to something that is false. See my reply to the grandparent.
Unless you have a very loose definition of"no one" that simply is not true.
Just off the top of my head:
Haxl at Facebook Bond at Microsoft Supply chain management at Target
Also see:
What part of "to a first approximation" was unclear?
https://www.tiobe.com/tiobe-index/
Haskell is in 47th place, which is consistent with where it ranks in every other popularity list I've ever seen.
I'm standing behind "to a first approximation, nobody".
Note that I'm not saying that Haskell is a bad language, or that Haskell programmers are bad people or anything like it.
I'm saying that the vast majority of programmers do not use Haskell. An anecdote about a particular group that uses Haskell (or even several groups) does nothing to refute that fact.
I think you're dismissing the post without engaging its arguments, so it hardly seems fair to start calling people naive, anti-intellectual, and ignorant. (btw, we all get that these are different ways of calling someone stupid, which is never productive and isn't justified in this case.)
To attempt to engage your argument, as far as I understand it... i think type systems and programming paragidms, however formal, can at best solve problems only in a corner of the problem set of software development. The limitation is because these do not take into account various kinds of constraints on software systems which nevertheless exist and are often the dominant constraints, depending on the project... Requirements, maintainability, usability, estimation, etc -- most of the stuff above the red line from the article.
I like Idris, and there's room for these languages. I think you give them too much credit though, programs written in them still have bugs. Your spec can be wrong. But above all else, they can't help you with scale, performance, recovering from hardware faults, and delivering what users wants.
The languages are still new, they'll gain traction, and for certain use cases they'll make sense, for others they won't.
"Today a usual technique is to make a program and then to test it. But: program testing can be a very effective way to show the presence of bugs, but it is hopelessly inadequate for showing their absence. The only effective way to raise the confidence level of a program significantly is to give a convincing proof of its correctness."
"Beware of bugs in the above code; I have only proved it correct, not tried it."
For example, the Single Responsibility Principle (SRP) is primarily concerned with making software more manageable on both an individual and team basis. How? By minimizing:
1. Communication overhead between teams/modules
2. Information overload in an individual
You could look at #1 from a graph-theoretic and information basis. I'm sure there are many interesting things to prove there. Like Amdahl's and the opposite of Metcalfe's Law [1][2] applied to team/communication/module dependencies. Just as a basic example, if one class has 10 responsibilities shared by 10 engineers with no boundaries specified, then the probability of conflict and unintended consequences rises. Thus the rate of development slows.
As for #2, applying more rigor and proof to the question of how these principles help a human understand quicker.
I don't have the necessary background right now to explore this in more detail, but like you, I'm very interested in any possible formulations.
I am not a full subscriber to SOLID. I think it promotes a certain kind of degenerate over-abstraction that leads to bugs of a different nature, premature decisions on what needs future substitution, and decreases agility in the medium term.
But the actual practice of doing mathematics (i.e. coming up with novel proofs) works exactly like this as well. The differences are in how much confidence we have in the results, and how much we're able to reuse them.
> It's also self-evident that in most situations, correctness and reliability aren't a concern. The counterexamples account for maybe 1% of the field. 99% of the time, if your program breaks, you can pay someone to go fix it and no serious harm was done. Even Github outages, which affect almost all of us, hardly matter.
I agree that we collectively don't currently care as much about correctness as we pretend we do. I believe software correctness is becoming more important (e.g. the rise of ransomware) and is going to become much much more important, but that's due to what I accept is a non-mainstream view of the future.
If those examples are 1% of software, they take disproportionately more funding than 1%.
And I'm sure customers of software, from personal computers, to business apps, to corporate websites would appreciate more consistent results as well. Reckless software engineering has damaged the reputation of the field as a whole.
Sounds a lot like engineering/design/art. There's a large amount of overlap between the three.
I had the pleasure of speaking to the principal electrical engineer whose firm was responsible for designing the entire electrical system for One World Trade Center in Manhattan and the Citi field as well.
He described his work a lot like a software developer would describe their own. And then, in his words, when his company was done they "passed the plans over to the electricians to build it".
It just so happens, in our profession, we've automated the part that electricians are responsible for in his project. Our electricians are called compilers. They dutifully carry out the plan and from time to time they surface warnings/errors back to the engineer for input/correction.
People conflate the meaning of software development because one person shares so many different responsibilities, that are usually handled by separate people in other professions: architecture, design, analysis, implementation, maintenance, etc.
What a civil/electrical/mechanical engineer does isn't so different from what a software engineer does. It's a "scattershot haphazard endeavor that involves trying dozens of angles [based upon guiding principles] until one of them works" usually run through loads of simulation and analysis. Now, the difference is, when these engineers want to bring their idea into the world it takes physical labor, unlike software development where the feedback loop is near instantaneous. We bring our programs into the world with compilers and can run them immediately.
I mean, there are plenty of examples where civil/electrical/mechanical engineers failed in their design and thus created a bug in their project. See [1] or any contemporary CPU from AMD/Intel or automobile recalls or spacecraft failures, etc.
There are certain principles of software engineering that lead to more effective software. That's a fact. And the companies that understand this fact will not fail to startups, in fact they exhibit a severe technological advantage.
Google and Facebook are two companies that understand software engineering. Talk to the YouTube/Instagram teams and see whether they felt better off -- technologically -- before or after acquisition.
[1]: https://en.wikipedia.org/wiki/Citigroup_Center#Engineering_c...
[1] http://www.developerdotstar.com/mag/articles/reeves_design.h...
I don't think this is self-evident whatsoever. One of the problems in software engineering is that we never know when a solution is "right," we only know when it's vaguely not-wrong, and even then almost everything we create is still subtly wrong in a way we forgot to think about. Math is solid because there is certainty in the correctness of certain proofs, and these can be used as building blocks for further results. Philosophically speaking this is the closest we're going to get to "real" engineering practice in software, and we're pretty dang far from it if you know what that looks like.
>Software dev is generally a scattershot haphazard endeavor that involves trying dozens of angles until one of them works.
But this is a symptom of any pre-scientific field in engineering, it's not specifically endemic to software engineering. The main difference is that in software engineering we're applying math directly, and in other engineering fields we're applying science. In a certain sense, the natural sciences are purely empirical (modulo advanced physics of course, which overlaps with pure math and philosophy these days) while math and consequently computer science are purely rational. So, what are the solid elements in math? Proofs. Proofs are also how you ensure that the field actually moves forward and you're not stuck recreating solid results that already exist. Sound familiar? It happens constantly in software, but imperative and poorly-typed languages inhibit composability and reuse because they lend themselves easily to extremely specific solutions to general problems.
>It's also self-evident that in most situations, correctness and reliability aren't a concern. The counterexamples account for maybe 1% of the field. 99% of the time, if your program breaks, you can pay someone to go fix it and no serious harm was done. Even Github outages, which affect almost all of us, hardly matter.
This is preposterous. Just because lives are not in danger does not mean that it's not worth doing right by the solution, and frankly I think a lot more lives are waiting to be put in danger by crappy software with bad security than you realize. It's already become almost dogma that all software engineers need to have a deep understanding of security, and I don't understand why correctness can't fall under that rubric as well. If we're going to be having Geohot or even Google or whoever building self-driving cars for possibly billions of people, enormous critical infrastructure projects coming under computer control, etc, the whole industry from education on up is going to have to have a serious attitude adjustment to keep up with the demands of safety, security, and reliability.
It might not matter 99% of the time, (I think it's a lot more than that of course) but we need to make sure that we can as a discipline deliver that 1% when it is absolutely critical, and as of right now it doesn't seem like we can.
FWIW, we agree on this point. But it seems worth treating this 1% case as a separate discipline rather than trying to lump it together with software dev. No one would claim that NASA's software engineering is the same type of work as, say, writing a new HN feature.
It's already become almost dogma that all software engineers need to have a deep understanding of security
The most secure programs are those that undergo frequent penetration tests and have bug bounty programs. Speaking as a pentester, I think there's not much chance of regular software devs being any good at security. There's just too much to know.
I want to agree with your other points, because in principle it's the correct thing. Unfortunately experience has taught us that the correct thing usually loses in the real world. Being first to market mattered way more for Ethereum than the fact that the DAO had a bug in their smart contract, for example. But there are hundreds or even thousands of examples of this type.
If we pretend that a teenager hacking in their bedroom is doing something fundamentally different than what most developers do each day at their jobs, then we lose out on the ability of that teenager to innovate. We become an exclusionary clique rather than an inclusive group. Luckily market forces still prevent us from becoming that insular, but in the era of walled gardens it's easy to imagine we're not too far off from that fate.
The main issue is that if we try to restrict the free market e.g. with legislation, then the important work will simply move overseas to areas without those restrictions. And unless you're proposing legal restrictions on the software dev trade, it's unclear how to enforce any of the proposals upthread.
Well no, but the same underlying principles are still operating. The only difference is how much you care about heeding them. You don't need an aerospace engineering degree to make a paper airplane or a short bridge or a raft or whatever, but that doesn't mean that your knowledge of how to do so reliably and correctly wouldn't be improved by such a degree, or that if you're going to sell a product that you hope people will pay you for and subsequently depend on that you shouldn't bother trying to make it functional (in the "it works" sense) to the best of your abilities.
>If we pretend that a teenager hacking in their bedroom is doing something fundamentally different than what most developers do each day at their jobs, then we lose out on the ability of that teenager to innovate.
Ok, that teenager can hack, sure, just the same as they can build a two-stroke engine or an electronic alarm for their door or play around with nuclear fusion or whatever. But if they're going to sell those things and make claims about their safety and reliability, the validity of those claims should be enforced by an industry guild accreditation program or legal regulations or whatever. There's more than one way to skin this cat, but it really needs skinning.
>The main issue is that if we try to restrict the free market e.g. with legislation, then the important work will simply move overseas to areas without those restrictions.
The goalposts are being moved here, though, near as I can tell. I told you what I wanted done and why I thought it would work, and now you're telling me I have to figure out how to do it specifically in such a way that it can't be circumvented. I haven't thought up a specific solution to this question you pose, and as such I would point you in the direction of how liability works in other disciplines for similar cases and so on. I do actually think a lot of the same systems could work for enforcement, the biggest difficulty is actually figuring out what the principles should be. If the biggest problem with enforcement is that teenage hackers can't innovate anymore, I'm not really all that concerned. Romanticizing that image does nothing to change the hard realities of the industry.
Not really. The time scales are completely different: that HN feature that is schedule a week of dev time is incomparable to that probe feature that is scheduled years of dev time even if the amount of code involved is the same. You could argue that both are "just programming", but the activities and process involved in both are going to be completely different.
You missed the point though. Whether it takes you five minutes to code the feature or fifty years, you're still doing math. The so-called "engineering" principles might change, with regards to division of labor and so on, but the underlying science/math you're dealing with doesn't significantly.
In engineering the time it takes to implement the design/proof/code/output is one of the constraints. In math this constraint is ignored.
That all contributors don't have the capability to formalize their output has never been a viable argument against formalization.
Before music education was formalized music was a mysterious craft you could only learn by learning with a master for a decade if you weren't incredibly talented.
Once the orphanages of Naples formalized music teaching in the 17th century it became something much easier to learn and teach.
Sound familiar?
Yet, music teaching did not eliminate the capability of non-formal craftmen to innovate. They just have collaborators to help formalize their thought process.(John Lennon did not know music theory and still made awesome stuff. But without formal theory his output could not live on in sheet music, and it would be a lot harder to reproduce it).
Even Einstein needed help with his math. But without math, theory of relativity would not have been much of anything.
It's all fine to imagine one is traveling in a traincar, but once one needs to compute, say, the orbit of mercury all need formal methods.
Creativity and formalism go hand in hand. You need both for a superpowered discipline.
I have over 30 years of experience and I couldn't agree more. The security field - heck, the website security field - is way too complex for me to navigate it properly. Sure, I know about SQL injection, but "authentication is not authorization" is something I tend to forget, and I am pretty sure I have no clue about at least half of OWASP top ten.
This way, I think formalizing software development is a worthwhile goal - just like formalizing cooking is - but it's also obviously so uneconomical that we can't expect the industry to bother with it. Formal methods are pretty much basic research - not useful for us in any meaningful timeframe, but hopefully our grandchildren will get some mind-blowingly amazing tools out of it.
It is a way to solve mathematical problems, See "Guess and Check" from this book https://en.m.wikipedia.org/wiki/How_to_Solve_It
Maybe in an agile web startup. SW engineering in a big industry project is a very deliberate process. You start by a requirements engineer writing very precise requirements. Then a SW engineer turns this into a module design and a test specification. These are turned into source code (for which we use code generators to an ever higher degree) and test cases by yet other SW engineers. In the end everything gets reviewed and/or tested.
Trying things until they work is just not done. That would be way too dangerous for SW that controls cars, airplanes, nuclear power plants, rockets etc.
There are hugely more systems not written to that standard.
So software engineering isn't engineering, either? I would imagine any civil engineer who actually knows what it takes to build a bridge would tend to agree, at least on the basis of the points you have put forward so far.
I bet if we fast forward 1000 years, you'd find that software engineering will have become as rigorous as what we have today in civil engineering.
How is that not like software engineering?
But in the software world, it seems the equivalent of the cold is a CRUD app, but still fails so often that it's newsworthily talked about when such a software project succeed!
This isn't evident at all. In software, every situation is novel, so there is no room for repeatable processes.
You can build a "bridge library" once and tweak it for each situation, but you never need to develop a rigorous process to build that library again.
this is the point i m contesting - that most situations aren't as novel as the stakeholders think it is. The failure happens because the assumption that it's novel is there!
I can potentially lay down a bunch of assumptions, and prove that, given those assumptions, my program acts correctly. However, most of the bugs arise from incorrect assumptions.
One concrete example: When feeding pixel data to the onboard hardware h264 encoder's driver, after having set a resolution of 1920x1080, the resulting h264-encoded frame will be displayed in a h264 decoder with a resolution of 1920x1080. This turned out to be wrong, because the hardware can only deal with blocks of size 16x16, so the width and height must be a multiple of 16, and the driver isn't smart enough to add the necessary metadata to make a decoder crop it, so there's 8 green (because YCbCr) pixels on the bottom of the video. The solution to this is to manually splice the h264 bitstream, to insert my own metadata which has the correct cropping. How the fuck do you formally prove any of that?
Well you basically answered your own question - you would need a language with a more sophisticated type system. You would then need an API/DSL to interact with the graphics hardware.
I suppose that life is irregular.
Not OP but all pre-scientific crafts from medicine to construction have benefited considerably of application of formal methods. I don't see why software engineering a should be different.
Anyways, surely SE as a field benefits from formal methods like other fields, whether applied by specialists or in the field by practitioners we can debate, but hopefully we can all agree SE isn't defined as just applying formal methods, that there is a lot in development that will never go near a formal spec.
I've yet to see a field without artificial restraints that has abandoned need for human intuition and creativity.
>they are for programming (as in math) a well-defined, solid formal system that solid systems can be built on
Except you forget one big thing. Maths do not deal with errors or real world complexity. Maths exists by themselves in a world where errors and failure at other level do not exists. And i will not even talk about Gödel incompleteness or Turing proof of the the halting problem as other fundamentals mistakes here.
> can be built on in a way that nothing else can be in software, at least thus far. What about System Engineering? Because guess what? Other complex systems exists in the Nuclear, Space, Chemical or Aviation industry. And they are not developed with formal proof... and they still do work... But they use Engineering, proper one. Not wishful thinking and all.
>In a world where software flows more freely than water, the correctness and reliability of software systems must be taken with utmost seriousness. There is a really really small but essential mistake here. Two to be honest. The first one is that any sufficiently big software can not be proven correct and reliable. That is what Complexity Theory tell us.
But most importantly, it does show a complete lack of knowledge of the meaning of the word reliability and the research in Complex System. Reliable and Correct systems are inherently dangerous. What you want is a system that is SAFE. A system that is Safe, is a system that accept to do the "wrong" thing if it is the safe things to do.
>What do you propose as the theoretical basis for the engineering science of software development? Complex System. SNAFU catching. Stop trying to ignore the stack we live in and begin to think about runtime instead of over complex architecture. Safe guards and operators. Debugging as a first class citizen. Bulkheading and recovery. In general, System Engineering and Human Factors.
You can begin with reading web.mit.edu/2.75/resources/random/How%20Complex%20Systems%20Fail.pdf then follow with Nancy Leveson free book https://mitpress.mit.edu/books/engineering-safer-world .
PS: oh by the way, to everyone saying that other Engineering discipline are based on rigid step-by-step methodology that enforce correctness. It is not. It is even more a mess with slower feedback loop. I worked in other engineering fields before IT and it is not really better. It seems to be really American to believe in the "scientific method". But that does not exist. The world outside is messy and complex.
Try accepting that. There are solutions, but by living in a dream, you are working around the bug instead of fixing it.
Computer programming is not a special snowflake. It's a field that (in many areas) refuses to grow up.
It's important to keep in mind what "growing up" translates to: slowing down. This has both economic and competitive implications. Sometimes it might be a win, but the vast majority of the time your ability to move quickly (and yes, occasionally break things) is an advantage.
For example, a program must run on a platform that doesn't have everything formally defined or have guarantees. If a program relies on that platform and that influences the program in a way that makes the constraint reliant on the platform, then you are out of luck.
Another issue is choosing the constraints that the program will operate under. You would hope that the clients would give you the requirements including the constraints the software must operate under. But this isn't often the case. Having an incremental approach which includes clarifying requirements by mapping what the clients need to do to get their work done, which includes recording the specific steps that they perform or need to perform works pretty well when clients don't provide the requirements or constraints upfront.
I am relatively ignorant on formal engineering, but I do like that you have provided a fairly clear definition, which was "Clearly define the constraints in which your project will operate under and prove that they will hold under those constraints". It is better than the people saying know more math, without saying how, or what, or why it is useful in any clear way, and saying software is math just doesn't cut it.
Choosing the constraints for a project is no different in the context of CS than the context of any other fields -- electrical, mechanical, etc. It is a conversation, as you stated. This helps in many ways: it helps the developer understand exactly what the client wants, helps the client understand exactly what they are going to get, and helps build an implicit timeline replete with discrete and obvious deliverables and (if done correctly) those deliverables are fairly modular.
Thanks! I, too, get frustrated that people just say 'math! math! math!' That isn't helpful or meaningful. This is a conclusion I came to after talking to quite a few of my friends and colleagues in different engineering disciplines.
A little off topic, but it would be great if there was a method/system which could provide requirements tracking down the set of artifacts to where you could point to a bit of source code and say it implements that certain requirement. Sort of like a chain of responsibility for code and associated documents. That might be a pipe dream, I don't know.
Anyway, thanks for the information, I remember seL4 being mentioned in discussion of the sorry state of software on medical devices, but had forgotten it until you mentioned it. Thanks.
Every other discipline does simulations because actually running the experiment is magnitudes more expensive and time consuming.
See "Why software development is an engineering discipline"
https://www.youtube.com/watch?v=zDEpeWQHtFUNo, what turns programming into engineering is having a rigorous understanding of proof methods and being able to apply them to solve problems the way solid science is used to solve problems in other engineering disciplines. Civil engineering and electrical engineering and mech-e and so on became engineering through the discovery of underlying principles that allowed processes to be formalized, standardized, and improved.
Formal methods have to be at least part of the answer here, unless you can think of a better way to formalize, standardize, and improve the process of software development.
To believe that, you have to believe that simply adding maths to something turns it into engineering. I think this is fairly obviously not the case.
You're also misunderstanding me if you think I think "adding maths" to CS will turn it into engineering. We're already doing math! I think CS could be made a lot more solid by being honest that we are doing math and adopting the relevant formalisms that already exist to make reasoning about mathematics easier.
Do you just disagree that that would help, or do you reject the premise that it could be made better entirely?
Now what does make mathematics slightly more rigorous than other disciplines is the fact that once someone bothers to actually work through the details and finds a counterexample, they can convincingly demonstrate to other mathematicians that the proof is incorrect. Often, the detail in question isn't even all that important, and a workaround can be found that saves the overall proof. But software development is also rigorous in this sense; once you find a case the program handles incorrectly, you can write a testcase to show the difference between expected and actual behavior. And that doesn't usually show the whole program to be misguided, you can just rewrite a small part and things work again.
You seem to want a method that can not only make definitive statements after the fact, but that can actually ensure for almost all programs and almost all desirable properties that the program fulfills the property. But this is actually much more rigorous than most mathematicians ever bother with, and for good reason.
Complete verification requires stating every obvious fact in excruciating detail, because that is the only way to be sure that it is indeed obvious and a fact; in addition to tracking the complex interactions of the whole thing. Most humans really don't want to make this kind of mental effort, if they can avoid it. Even static type annotations are too verbose for some, which has lead most modern languages to include some form of type inference. I don't think you will see widespread adoption of formal methods before proof assistants are developed that can similarly handle most of the simple but tedious tasks, so that humans can focus on the actually important bits.
It's also not specifically the rigor in mathematics, but the grounding in solid principles. They have axioms, they know how to prove things, and they know which proofs to trust and why for the most part. What frustrates me most is stuff like programmers haphazardly reimplementing monads over and over again instead of moving on with what they were actually working on before the language and type system got in their way.
Where did the formal specification come from?
How do I know the formal specification is what I actually wanted?
Is the connection between the informal requirements to the formal specification easier to trace/follow than the connection between the informal requirements and the code?
There are two separate problems here - one is that you might not be able to clearly explain what you actually want. The other is that you might simply fuck up when writing the formal spec (code). Formal verification is meant to assist you in the latter - when you know what you want, but can make mistakes writing it down, or not realize your description is self-contradictory in some aspects.
I'm working on a radio product, it's clear how data is being moved into certain buffers. It's clear when data is moved into certain buffers. It isn't clear why data is moved into certain buffers, or if the code is correct, only that it's being done.
A higher level specification set allows us to have a documented understanding of why the code does what it does, and allows us to reason about it at that level. It also makes it feasible to bring new people into the project, because 150k sloc (not a huge project, but not small) of largely low-level code is not something someone new can jump in on and understand quickly.
We also have something that's much easier to reason about when designing system tests, and to test the code against. We write the tests as though the specification were the reality, and test the code against that model to detect where it diverges. If we only had the code, what would we test it against? If it's its own spec, then it can't be wrong.
Yes, people tend to forget that. Having a second formal specification can be helpful, because writing things down multiple times (differently) often helps understanding.
What I've seen so far is that (non-code) formal specs can be very useful when the domain is highly technical, for example network protocols, because they illuminate aspects that are hidden in "production" code.
Of course the fact that important aspects are hidden is a more general problem.
With that said, if Microsoft Word meets the given spec, then it's correct. One way to prove this correctness is with testing.
This is the case for bridges as well. If I hand a spec to an engineering firm requesting a bridge from A to B at any given price. Well then, there's a lot of bridges that satisfy those constraints.
Just because many software companies today don't choose to formally specify a spec and prove a programs correctness upon delivery doesn't mean it's a special snowflake. It just means those teams are immature.
Sometimes software development doesn't require a mature team. Like most decisions, there's a cost and timing tradeoff.
The problems that matter are in the design of the spec to begin with. The important part is picking the CORRECT business requirements, NOT in implementing those business requirements correctly.
And do you know what the best way is to test whether you got the spec right? You deploy and see if the feature gets traction.
The "spec" that matters is the success of the business.
And building a product, and releasing it, is the way to formally test if your feature is "correct" according to the spec that is The Market.
It's both, though. You also can't tell if you've implemented them correctly if you don't have a formal spec.
If I make a mistake building my web app, then it will either not matter, or someone will notice the bug in production.
And then when someone notices the bug in production, it can be fixed. If nobody notices it, then I guess it wasn't very important to begin with and can be left "broken".
Implementation bugs are the EASY part, and don't matter a lot of the time.
Or here is a better scenario.
Lets say I am writing a feature, and I think of a way to implement the feature much quicker, but isn't 100% "correct" according to the spec. The quick and dirty, but "incorrect" way to implement it may actually be a better thing to do, because now I can spend my time working on other stuff that is more important.
Purposefully doing the "incorrect" thing according to spec, may actually be the right decision.
You just described the responsibility of a product manager, and finding product-market fit. None of which requires software development. Software development may help but product management certainly doesn't require it.
Designing and building software are now the same thing. And that is only going to become increasingly true. Designing solutions in the context of modern systems inherently requires intimate knowledge of those systems and the capabilities of the technology being used to solve the problems. The "design/spec/build/test" pipeline is dying.
You can recognise that that's a good thing and get on board or you can be left behind.
You misunderstand what a spec is. And you misunderstand what product management is. At no point did I say software engineers aren't responsible for designing and building software. And at no point did I say designing solutions doesn't require intimate knowledge of those systems and capabilities. In fact, that's exactly what I've been saying.
That's what software engineers are there for. To provide expert knowledge and guidance.
But, do you think the electrical engineers defined the spec for One World Trade Center? No they didn't. They got the spec from the architects and they worked to satisfy those requirements.
The spec is not static. There is no design/spec/build/test pipeline in the strictest sense. The spec is dynamic. It's updated through design/spec/build/test iterations.
Just like an electrical engineer may surface new knowledge back to an architect that requires the spec to change... or an electrician in the field will surface new knowledge back to the electrical engineer that requires the spec to change.
Changing the spec is expected. It's called change management.
I don't need to get on board with anything. Google isn't getting left behind anytime soon. And the way they approach software engineering is largely the correct way; I agree with it. (They do however lack coherent product management in some areas.)
Product development skills are extremely important for a software engineer to have, especially at smaller companies, because a lot of the time the person making these product decisions IS the engineer.
During my engineering career, most of the time my boss gives me a general goal for a product or feature that needs to be built. And then I take that general idea for a product, and make all the product decisions about what to build and how to build it MYSELF.
At smaller companies there may be NO product manager. Or maybe the product manager is only making very high level decisions, and isn't really involved in every little nitty gritty detail about the product.
You the engineer have to make the product decisions. And you have to balance those product decisions against tradeoffs, such as how long would it take to build, how high quality it is, and other software engineering design tradeoffs.
Product design and software engineering are very closely related, and any good senior engineer should be competent at both. Software engineering makes you better at product design, and vice versa.
Yes, most startups don't formally define their spec. That's what I've said.
Managing the spec and ensuring product-market fit falls under the domain of a product manager.
So, that's great, you did software development and product management. You wore many hats... like most people do in startups. Doesn't negate the fact that you were a software engineer taking on additional responsibilities.
Trust me, when you work on a team with a clear separation between product management and software engineering and you have a great product manager... it is pure bliss. The only company I've ever felt that technical nirvana with was Google. My god they know what they're doing when it comes to software engineering and separation of responsibilities. At least the team I was on did.
For example, I can have a requirement that says: "The program shall generate a set of weekly time schedules that are maximally preferable, based upon each students' preferences, for all students at a given location while taking into account resource constraints re: room availability and teacher availability." Of course, this isn't specified to the level of detail I'd put in a real spec, but it serves as an example.
There's many ways to solve this requirement, i.e., there are many different programs that satisfy this spec.
There are two solutions that may stand out: (1) a brute-force approach, and (2) a convex optimization approach.
Since I've not explicitly defined a speed of execution requirement in this spec, then a brute-force approach may make sense... even if it runs for 5 days. In the real-world, you'd confirm this undefined assumption.
If instead my spec said this needs to complete within a day, then maybe the convex approach would make more sense. However, you'd first seek more definition in the spec, i.e., how many students are we generating schedules for? If it's only 10, maybe brute-force, if it's 20k, then convex.
So on and so forth.
Now, the interesting part comes when you create the end-to-end (E2E) and acceptance tests. These tests should be the first thing you write because they follow directly from the spec. They will stand up the program as if it's running in production and drive it as such to test whether it adheres to the spec.
Once all your E2E and acceptance tests are passing, and we've eatablished that your tests cover the spec completely, then we can mark the program as correct with respect to the spec.
There are many different software designs that satisfy a spec.
The software is not the spec.
Put another way, the problem with having a "software spec" is that you already have the "software which is a spec" and now you have 2 specs.
Or a 3rd way, figuring out the right interface for 2 components is at least 50% of the work when writing software. So, spec writing is like programming. And you wouldn't want to program by committee, would you?
This is one thing Amazon got right - having small internal departments and interacting like separate companies.
Spec writing is not like programming, and if it becomes like programming, then you're doing it wrong.
Specs are meant to constrain the visible solution space by defining the problem sufficiently.
To put it in programming language terms: a spec is declarative not imperative.
Though imperative programming looks at the problem from another angle which is closer to execution details, it's not fundamentally different. A smart compiler/interpreter may completely ignore those details as long as it produces the right output, as specified by the spec. That spec being the code.
This is obvious when you see that one style of program can be converted to another style without losing the semantics.
> whether the output solves the problem rather than whether it satisfies some arbitrary behaviour
The spec is considered the solution to the problem! It's not arbitrary in any sense of the word.
The problem with "specs" is that you don't know whether they solve the problem until the solution is implemented and shipped. And even then, you have no real way of knowing what's meat and what's cud. So lots of time, money and people are thrown at solutions that - at best - are wildly bloated or inefficient and - at worst - completely fail to address the actual problem at hand.
The _need_ for specs is - even in large organisations - typically down to misplaced accountability. When you decompose the problem space into small pieces and give development teams a high degree of problem-solving autonomy _and_ accountability for production, the organisational disconnects that lead to the "need" (or, rather, the ill-conceived desire) for burdensome process and specification largely go away.
This isn't witchcraft - it's progress. It works; and it works in large organisations. You haven't witnessed it, so you don't believe me. If/when you do, I'd be willing to bet you'll be converted as I was.
But I'm sure I've given you plenty of reasons to double down on your skepticism.
Please, do detail.
> The problem with "specs" is that you don't know whether they solve the problem until the solution is implemented and shipped.
No. Good product management eliminates this risk. And that's what you're talking about: risk.
You can test a product, feature, anything, many different ways before you build an actual implementation.
That's basic product and risk management.
> And even then, you have no real way of knowing what's meat and what's cud.
Monitoring.
> When you decompose the problem space into small pieces and give development teams a high degree of problem-solving autonomy _and_ accountability for production
You just like... defined what a spec is... man.
> This isn't witchcraft - it's progress. It works; and it works in large organisations.
Please provide the proof to back this up. Otherwise it's a baselsss claim.
> You haven't witnessed it, so you don't believe me.
No, I've arrived at my beliefs through the data on this point.
And the fact of the matter is that 100+ successful companies that have shipped successful products/projects operate with specs across many different industries from pharmaceuticals to construction to aeronautics and so on and so forth.
If the data supported your conclusion, then I'd agree with it. But the data does not support your conclusion.
This whole discussion can be replaced with this sentence.
Please tell me, what is the specification of this code so that we can verify and validate it:
(defun f (x y) (* x y))
Perhaps. Perhaps it was supposed to be addition. Perhaps it was only supposed to apply to integers. If the above spec is correct, is the code correct? Maybe. It doesn't react well when given non-numeric values. Is that a problem? I don't know, the code doesn't explain who is responsible for validating input and who is responsible for handling errors.
A specification is a hybrid prose/formal document that would give us all that information (if it had any value). The code above is not a specification, it is an implementation. No different than a gear or a cog or a lever in mechanical engineering. It is a thing which does some work. We can examine it and see what it does. But we cannot, by observation or execution, determine why without greater context. That context is the specification.
The software is an artifact, one among many, which (hopefully) satisfies a specification.
Can we use those? By your criteria, I mean.
You need science to come up with it and engineering to apply it in practice.
> why the author is so suspicious of
> formal methods
I think those of us who promote formal methods need to remember this. At best only verification -- making sure the implementation matches the specification -- will ever be fully automated. Validation -- making sure that what we specified is actually what we wanted -- will always be a human activity.
By the way, Curry Howard is just one way of doing formal proof (one I personally don't like). There are many foundational and practical problems that need to be solved before formal proof is ready to go mainstream (but I am convinced that it will one day).