Everywhere you go, you find these memes where developers are skeptical of their work. Things like "It works. I don't know how. It doesn't work. I don't know how.". Don't you guys think this is a huge problem? And people say that their programming language is the best, because preference. But isn't this happening because our tools suck?

Yes the problems maybe inherently complex but at least we should be able to figure out the logic behind the snipper and reason about it.

Haven't really experienced it, but they say Haskell and the likes are great at this and it must be true because it's backed by mathematical properties and laws, not " experience".

So the rant here is, wish we had better tools in the mainstream that allowed us to enjoy absolute faith in at least what we have written, regardless of the fact that we understood the problem in the domain.

A former co-worker always said, "computers are funny, they do exactly what you tell them to do. EXACTLY.." I think the problem is just human error. :-p

Issue here exists because of the fact you forgot what you asked the computer to do, asked it to do something else mistakenly, etc. At least, we need the tools to guide us to let us write and comprehend what we mean, even if what we tell them is wrong for the problem at hand.

I think the reasoning behind those memes is, at least from my perspective, as a developer there are constantly changing requirements that require different tools. It's impossible to know all the languages and if you're exposed (or required to use) to X because of a project, you may get it to work, but not fully understand why it works the way it does.

That's quite true. Management and marketing really arse us developers. So much so that we lose the freedom to choose the tools that we need! And client requirements are tough and dynamic. Even though I've just done a lot of reading, pure functional languages like Haskell seem very promising. Even all the great new tools rose from the concepts of the languages of that family.

Wish these were adopted well so that we no longer have to pretend doing any functional stuff.

That's the area I am doing my master's degree in: software verification and reasoning.

The problems are inherent, though. To gain perfect confidence in the code, you should be able to (a) specify precisely what it should do (b) prove that it fulfills the specification. Neither is feasible for arbitrary real-world software. As you suggested, almost nobody even tries to achieve part a, given the complexity and dynamics of the real world (but Amazon did, and had a very positive experience).

You may hope to be reasonably sure of part b, but actual proof is surprisingly hard and reveals intricate problems and hidden assumptions even in seemingly straightforward, "obviously correct" code. So even when you are "sure", it doesn't mean too much.

And I didn't mention deadlines and other constraints put on the dev's shoulder.

So why does a developer write code he is not sure about? Maybe because he has little time to think about it, and he knows that it can be done "roughly this way".

As for tools, you may write your program and prove it using COQ. People do this. But it will take you many person-years to write a medium-sized program - assuming you have mathematically-inclined devs. Until then, requirements will change thousand times.

You can specify and check your algorithms using TLA+. That's actually feasible, but not yet common. And it won't assure you that the actual code is correct.

And, of course, the what will ever assure you that you and your client think about the same thing? Will he read the Formal Spec?

In general, and sorry for the theory here, Rice's Theorem state that no non-trivial statement about programs can be computed. You must deal with false positive or false negatives or both.

Functional programming eases certain kind of reasoning, but is definitely not a silver bullet (there isn't one). In particular, you give up many developers that are not accustomed to it.

@elazar thanks for sharing this. Appreciate it man

@liveCoder you welcome.
Last point: even "perfect" software affects the very same world it works in. So the success of a perfect software may invalidate the conditions it was based on - changing its own requirements.

Thank you very much for your comments! They're truly informative. Have heard about Coq but didn't know they could be used that way.

Yes, I really agree on all things you said. But I have mentioned about being able to at least reason the code that we've written accurately.

Functional programming is not the silver bullet, I do agree. They're tools and they don't help us identify the problem, we can only use them to deploy whatever solutions we've momentarily perceived to be the most suitable. There are a number of talks and papers I've watched and read that sold me the benefits of FP. Learning them is tough though but I believe they're worthwhile.

I thank you again for the mention of those keywords and the theory. I certainly will do some readings on them. It's amazing when your rant gets great comments like this.