Hacker News new | past | comments | ask | show | jobs | submit login

It is a special snowflake because the semantics and correctness of nontrivial programs are often in the eye of the beholder (is Microsoft Word or Google Search 'correct'?). This isn't the case for bridges, cars or toasters. It's not just a matter of adding magic engineering dust until programming is engineering.



You're missing the point though, formal verification ensures that a program hews to a formal specification (proof) which is well-defined and can be reasoned about. Whether the formal specification fits the problem is a different story, but seeing as you can neither prove you understand what the program does nor whether you understand the problem, I think getting one half of that dichotomy is really important to getting the other half.


I don't see how I'm 'missing the point' nor do I have anything against formal methods. They just don't turn programming into engineering - we're a long way from that and some of it has to do (in a completely unglamorous way) with the nature of programming. We just don't know how to turn it into engineering the way bridge-building became engineering.


> They just don't turn programming into engineering

No, 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.


what turns programming into engineering is having a rigorous understanding of proof methods

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 literally lopped off the second half of that sentence which does all the work. Of course the part you quoted is not the case, that's why it's not what I said.

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?


The thing is that math isn't all that rigorous either. Formal methods (i.e. computer-verified proofs) are still very much the exception. Proofs are written for other humans to consume, and details tend to be glossed over. Usually this is fine, because the readers are mathematicians themselves and can fill in the gaps, but occasionally this leads to a crucial counterexample being overlooked.

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.


I actually think dependently-typed languages like Idris are the most promising in this area right now, at least until proof assistants get a lot better.

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.


> formal specification

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?


Code is the formal specification.

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.


Code is a formal specification. You can have layers of such specifications. The problem with viewing code as the specification is that a lot of languages obscure the intent and only reveal the how.

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.


> Code is the formal specification.

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.


No, the correctness is in the eye of a spec. Now, whether companies formally define their specs is a different story. Many startups don't.

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 problem with this line of thinking is that the problems that matter are not related to 100% implementing the spec correctly.

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.


>The important part is picking the CORRECT business requirements, NOT in implementing those business requirements correctly.

It's both, though. You also can't tell if you've implemented them correctly if you don't have a formal spec.


Not really.

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.


Your notion of correct does not apply to everyone: for many of my projects, the implementation that goes against the spec but has higher traction is implemented correctly, and the implementation that follows the spec but has lower traction is implemented incorrectly. The spec is just someone's idea of what will have the highest traction - it doesn't make code that follows it correct.


No, you just don't understand the definition of correctness as it relates to software. Correctness -- like safety -- is formally defined. You might want to look it up.


Uhm... I was responding to a conversation about software engineering not product development. The two are orthogonal.

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.


Your job as a software developer is to solve problems with code - not to take the thing someone else designed and make it go. That line of thinking just doesn't work.

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.


Thanks for the laugh.

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 is not at all the case.

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.


Like I said: A may help B or B may help A, does not imply B requires A. Where A = software development; B = product management.

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.


But software is the spec. In many cases, if you can formally specify what a function should do, you have already written it.


You're misunderstanding what I mean by spec. A spec is made up of a list of requirements. This list of requirements can be considered constraints on processes, performance, features, limitations, whatever. Whatever makes sense in the world of the specifier.

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.


Thing is, the need to formally define "behaviour" like that is a symptom of poor organisational/team structure. If you have multi-discipline teams with end-to-end accountability for a complete product (or vertical slice of a product) then your "spec" can be replaced with a problem statement and all of a sudden people can start focusing on whether the output solves the problem rather than whether it satisfies some arbitrary behaviour.


I agree with that totally.

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.


Software is not the spec, it's an implementation... of which there are many implementations that satisfy one spec.

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.


I guess you have never heard of declarative programming, design by contract or logical programming, which explicitly does constrain the visible solution space by defining the problem sufficiently.

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.


It's blindingly obvious that you've never worked in, worked on, or managed a successful large organization (say >500 people || >$1B mkt cap) or a successful large project (say >5k man-hours || >50 people || >$10M budget).

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


Re: first paragraph - incorrect.

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.


> Re: first paragraph - incorrect.

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.


"But software is the spec."

This whole discussion can be replaced with this sentence.


There are very, very few languages (or few applications of every language) where we can honestly say "software is the spec".

Please tell me, what is the specification of this code so that we can verify and validate it:

  (defun f (x y) (* x y))
Is the specification: `f` shall return the product of two numbers?

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.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: