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.
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.
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.
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.
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.
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.)
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.
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.
> 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.
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.