I am sick and tired of the arrogant, willfully ignorant developers touting their FP horn and bashing OOP without any qualifiers. This is getting as annoying as Java people posting their design pattern nonsense as if it was something good.

If you know what a monad is, you should also know the founding ideas behind OOP.

http://userpage.fu-berlin.de/~ram/pub/pub_jf47ht81Ht/doc_kay...

The ideas make sense. Moreover, Kay has an amazing track record of saying unpopular things and being proven right in the long run. If you spend some time looking into it, you should see that his high-level intuitions about software architecture are proving to be correct, despite many of his critics. A lot of hyped-up modern technologies are implicit, ad-hoc, overly complex implementations of OOP ideas done without realizing they are such. The whole IT industry would be far better off if people took time to look into and understand the original ideas behind OOP.

1. OOP is a higher-level paradigm than FP, so people comparing them directly usually are missing the point to begin with. OOP systems can be implemented in functional languages or use functional-flavored components.

2. It is beneficial to model algorithms without using state. FP is very good that that. (Boring but practical example: LINQ vs loops and variables in C#. Functional LINQ pretty much always "wins", just like Streams always win in Java.) However, large-scale systems almost always have state. If you do not have some wise approach for handling it, your designs will have issues at system level. OOP is one such approach and at that level its ideas have a lot of value.

I'll edit this post later to add a few more points.

It's made me start thinking of programs more as multicellular organisms, or communities, where each part is responsible for a particular task. I think this is the core genius of OOP. It's not about classes or (Java) interfaces, it's about programs being communities of cohesive individuals with well-defined communication protocols.

edit to add: I think another key difference is in increasing the level of abstraction that you think about your program. You want to build a layer where you just say what should happen (the "declarative layer"), and keep that separate from the idea of how it should happen (the "implementation layer").

Low-level code correctness is overrated. With some experience it's trivial to achieve even in a crappy language like Java. Nothing except horrible syntax stops you from writing "functional" code in Java (and even that became easier in Java 8). This is what I and all sensible engineers I know are doing. In my experience, this "weak" version of FP plus a few tests is enough to virtually eliminate low-level coding bugs.

You can still get some surprising behaviors from 3d-party libraries and stronger FP can help with that a bit, but it's nowhere near as drastic of an improvement as many people present.

There are two big classes of errors I do often see in real life.

1. Spec omissions aka systems Broken As Designed. Your system works the way you expect it to work, but produces results users did not anticipate.

2. Emergent problems. Like someone shutting down your service for a day, causing queue backup, causing a huge batch of data being sent to vendor when the service is back online, causing vendor to throttle you, causing all other jobs being delayed.

#1 seems to be mostly a matter of experience and knowing when to show people some diagrams. OOP and especially agent-oriented programming can actually help you when reasoning about #2.

https://www.quora.com/Why-is-functional-programming-suited-f...

Functional programming is also easier to mathematically verify than imperative:

https://semantic-domain.blogspot.com/2018/04/are-functional-...

While you might not do proof, languages and methods that are easier for proof are often easier for automated analyses that look for problems, too. There's tools out there that can check code for concurrency problems that are extremely hard to spot with just testing. They might be easier to build or get more results if the program was functional/stateful instead of heavily stateful.

https://github.com/project-everest/hacl-star

You can verify stupid designs or smart ones. You can do impractical verification or pragmatic approaches. Formal verification is a tool whose outcomes depend on who wields it. The only consistent drawbacks it has are requiring more expertise, the project takes longer, and the project has to be simplified in design/implementation. High-quality software in general (eg OpenBSD) often has same properties, though. Possibly intrinsic to achieving correctness rather than additional requirement of formal methods.

Of course, you can still deadlock yourself; and read-modify-write can still be done in a racy fashion. Emergent properties of a system are still hard to reason about, but individual processes should be easy to reason about.

But... dynamic dispatch is a source of errors when it is very often possible to get the benefits via type classes, giving strong compile-time guarantees.

It's possible to understand "OOP is a higher-level paradigm than FP" in more than one way. I see no fundamental reason why you can't model the top-level interactions of a system using FP. And if state has been wrapped in a monad, you can chase the state through the codebase looking at the typeclasses inferred.

It's not higher-level, it just allows different types of abstraction. OOP is about procedural abstraction, ie. a set of procedures permits you to add new types, FP is about data abstraction, ie. a given set of data types permits you to add new procedures.

Most OOP languages are not pure OOP, so they permit some data abstraction as well, and FP languages with good module systems also permit procedural abstraction.

No it doesn't, not pure, typed OOP [1]. Unless you introduce dynamic types, then neither is more opinionated because you can just cast or dispatch at whim.

[1] https://www.cs.utexas.edu/~wcook/Drafts/2009/essay.pdf

See: "Closures And Objects Are Equivalent" etc.

http://wiki.c2.com/?ClosuresAndObjectsAreEquivalent

And

https://stackoverflow.com/questions/2497801/closures-are-poo...

To summarise, FP provides good reasoning in the small, and OO is needed in the large to orchestrate stateful services via protocols.

Re: there being no problem, that depends. Pure OOP has advantages and violating the properties often sacrifice some of those advantages.

That's exactly the assertion that I'd like substantiated. I don't think there's consensus on this. Sure, it's mentioned in the oft-cited "encapsulation, inheritance, polymorphism, abstraction" mantra - but so is inheritance, and yet prototype-based OO doesn't have it.

Personally, I would say that the only core principles of OOP are object identity (i.e. objects are distinguishable aside from their state), and polymorphism via dynamic dispatch. Everything else is optional.

There's also a conceptual argument: dynamic dispatch and object identity both require encapsulation. What do you think you're dispatching or comparing equality on if not hidden state?

Managing state is a central part of what FP systems do; a normal Haskell program is, in a sense, a function that returns an imperative program for handling stateful interaction. The stateful and stateless parts are clearly distinguished so that the problems associated with state can be managed more effectively and don't make it hard to reason about parts of the program that have no reason to be state-sensitive.

While the mechanisms are different, that separation seems broadly the point of most pure FP systems and many impure ones.

OOP, on the other hand, is clunky as a concept...

I don't have a strong opinion on the topic of OOP vs FP, but it's worth keeping in mind that people mean different things when they say OOP. Furthermore (and more importantly for this particular discussion), it also appears that people mean different things even when they specify they mean alan-kay/message-passing variant of OOP.

For many, it's something like Smalltalk and Ruby, with their very late binding and ability for objects to respond to messages even without matching methods. Others find Erlang and Elixir to be good embodiment of Alan Kay's vision. And the third groups seems to define it as "kind of like how bacteria communicate, and kind of like microservices", which is really too fuzzy for meaningful discussion.

In your link, Alan says: "OOP to me means only messaging, local retention and protection and hiding of state-process, and extreme late-binding of all things."

That is... quite vague.

But you are not staying in your pure OO-world nowadays. There's always the boundary issue where you are giving up your careful encapsulation and where state needs to be transferred instead of being hidden away in some object (like exporting to JSON). Poof, your encapsulation is gone.

Furthermore, may OOP languages don't deal with ownership at all. If I'm a constructor and someone passes me an object A or worse, a list of As. Can I hold onto that list? Should I make a shallow copy? Should I make a deep copy, because I need the A objects in the state they are currently in?

What if I have to work with 3rd party libraries? What assumptions do they make about that?

Can I call methods on objects from multiple threads? I need to rely on the documentation to figure that out or provide synchronization myself just to make sure I'm not breaking things.

Also, it is no accident that refactoring tools have become so popular in the OO world. If you need to design OO with 'change' in mind, you need to employ lots and lots patterns that make your code looks like new FactoryBuilderPatternVisitorImpl().

But with refactoring, hey, I can easily change my classes thanks to my IDE, yay! Too bad if someone then passes me data that only fits the old classes and too bad if consumers of my library are getting nasty surprises.

It is with everything in software: use the appropriate tool for the job.

OOP != Java.

>OOP is great if all you are doing is OO and if your solution to a problem is running a simulation (what OOP was invented for).

Most problems most programmers solve are simulation in some sense. Including DevOps. I wish larger number of people realized this. Things would become much simpler.

The problem with class-oriented languages like Java is precisely that they are horrible for making simulations. Been there, done that.

>There's always the boundary issue where you are giving up your careful encapsulation and where state needs to be transferred instead of being hidden away in some object (like exporting to JSON). Poof, your encapsulation is gone.

Solving boundary issues is what OOP was designed for. Like, that's literally the original goal of the whole concept, as explained by Alan Kay many, many times.

You were able to send objects over the wire in Smalltalk in the 70s. Every time you open a webpage with JavaScript you're performing an ad-hoc reenactment of the same idea. The fat that this idea is implemented badly on the web doesn't mean this is a bad idea.

>Furthermore, may OOP languages don't deal with ownership at all. If I'm a constructor and someone passes me an object A or worse, a list of As. Can I hold onto that list? Should I make a shallow copy? Should I make a deep copy, because I need the A objects in the state they are currently in?

This problem has been solved in 1978.

http://publications.csail.mit.edu/lcs/pubs/pdf/MIT-LCS-TR-20...

>Can I call methods on objects from multiple threads? I need to rely on the documentation to figure that out or provide synchronization myself just to make sure I'm not breaking things.

See the paper above.

BTW, guess how I found it? Alan Kay's talks.

>Too bad if someone then passes me data that only fits the old classes and too bad if consumers of my library are getting nasty surprises.

Again, getting rid of "raw data" was one of the core motivations behind OOP. See the email above.

I think I made it clear that OOP is fine if you can afford to live in that space. In practice you often can't.

Re the boundary problem: Sending objects over wire doesn't solve it at all, it makes it worse. Object identity for once and incompatible classes between client/server. Hiding data in magic objects just doesn't work. It's the reason CORBA failed, it's the reason RMI is a nightmare, it's the reason we have data-oriented wire protocols.

Works fine for billions of web pages that run JavaScript.

Actually, class-based handling of raw data can be done very nicely if you have multiple dispatch, which solves the so-called expression problem. Cf Julia.

I would really like to see some OOP language that implements James Reed's reference versioning or at lest a weaker implementation where every object "mutation" creates an effective copy with the changes, without touching anything that would be referenced previously. It would fix a lot of low-level annoyances people have with SmallTalk, JavaScript and so on. Would be extra amazing if it was based on prototypes, not classes. But at this point it sounds like I would have to write it myself.

Those structures don’t behave as objects themselves, but it’s not uncommon for Haskell monads, for example, to have very object-like behavior when you build them up a high layer, while each step in the monad is still an immutable value with cheap mutation-copies.

Are their any specific talks you recommend? I've only been exposed to OOP through Java so I'm curious to hear more about its roots

There is this famous talk from OOPSLA 1997:

https://www.youtube.com/watch?v=oKg1hTOQXoY

If you want to see what "practical" OOP looked like in the 80s, this is a good video:

https://www.youtube.com/watch?v=QjJaFG63Hlo

What is OOP language?

And even for simulation-like code (or really any other case of "very-high-level" code featuring "object"-like entities linked by complex, non-trivial relationships) ECS systems work a lot better than plain old OOP, while preserving the wide variety of advantages that you rightly point out. Especially since ECS works as a reasonably-thin layer over the usual sort of data-oriented programming.

I used to believe that. I no longer do. Among other things, I watched this talk about Overwatch's architecture and it really seems like you have to go against your OO instincts to create larger simulations: https://www.youtube.com/watch?v=W3aieHjyNvw

OOP as actually implemented and found in the wild isn't about Smalltalk or message passing. It's about transforming functions into methods by unnecessarily wrapping behaviour in classes, as an example of cargo-cult programming.

OOP the idea is great. How do you actually find it in the world?

Take callback hell. Opaque callbacks are the functional equivalent of goto statements.

Also, many functional programmers, particularly Haskell programmers, seem not to care about readability and maintainability. They're focused on maximizing their own productivity as an individual coder, and writing cool concise and abstracted code that might not actually be easy for another engineer to understand and modify.

The difference though is that good functional programming is still quite common whereas good object oriented programming seems to be rare (the one exception being microservices).

in some sense they are worse because you can't just grep for the call site of an anonymous closure, like you can for a goto, it could be almost anywhere in the code base

Say what you want about the foreign-ness of the syntax, but Haskell code is some of the most maintainable code out there. I can often times dive into another person's haskell code and grok it more easily than the equivalent code in a "friendlier" language like python or ruby, nevermind a more comparable language like scala. Haskell is also a breeze to refactor, the compiler and type system make changing and moving arbitrary chunks of code around pretty straight-forward, even when the code is using abstractions you're not familiar with; something which cannot be said for many other languages. The biggest downside to haskell (apart from the learning curve) is having to deal with cabal+stack.

To use OOP properly is probably as complicated as doing functional programming or data-driven programming properly. The "problem" is that the learning curve is much less steep and the use-cases more extense, so obviously there's a lot more people misusing it.

A cousin comment notes that true objects are often called "actors". This is fine, but people who do this without an understanding of this history may come to miss out entirely on objects, only seeing what Erlang and Elm have to offer and not E.

As a hint, try removing the meme entirely from your inventory for a bit: For the next week, whenever you think or say "object-oriented", interrupt yourself and instead think about what specific language feature, be it classes or inheritance or whatever, you actually wanted to reference.

[0] http://erights.org/

It works. It is a sufficiently good model for many domains, even though it obviously is "impure" by combining the domain model and generally a whole lot of implementation details nee requirements.

It clearly is an unreasonably effective strategy that has no solid theoretical footing, yet that does not prevent it from working in practice.

In terms of real programs in the real world, OOP in the form of Java/C++/C# is by far the most successful programming paradigm ever. It's sort of amazing that anyone would call it's track record 'abysmal'

Beyond that, failures all around. On top of my head:

* The insistence of designing systems fragmented in tiny state machines instead of systems processing immutable values passed around wholly and processed by pure functions. In the UI domain we finally got back to our senses with React.

* The insistence that values do not exist, but rather objects = data + code. Leading to brittle abominations like CORBA, agents, etc. For distributed systems, a humble RPC passing values [NOT objects] back and forth is infinitely more valuable.

* The insistence that inheritance is a useful design mechanism, leading to highly coupled codebases. Also, a prime cause for object-relational impedance mismatch.

* The insistence that one should overengineer code for extension without modification at every turn. How about just write the simplest version of the code for today, and refactor it if new requirements pop up.

* The insistence on messaging as fire-and-forget [aka goto] instead of structured function calls. Decades after we've learned why goto-oriented programming is a poor idea.

* The insistence on overusing polymorphism to mock everything in testing. Making it hard to trace how the codebase actually operates, and making it expensive to change the codebase because tests and code are tightly coupled.

* The insistence on overusing polymorphism for all type-based dispatch. Try writing a compiler in a purist OOP style, with a visitor for every type-based switch. Maybe it works in Smalltalk, 'cause in Java/C++/C# it gets boilerplaty really fast. Or even better, "encapsulate" your AST data into "objects hiding their internals" and do all type-based dispatch using vanilla polymorphism. Nothing screams "fun" like wading through tens of files to piece together what should have been a single switch block.

As for UIs, React is OOP. It borrows many ideas from FRP, but at its core are objects that have behaviour and state (components), and a system to orchestrate them. It might not be OO from 1990s Java, but it's definitely OO.

As for the rest, well:

* The concept of "values" form the basis for several important OOP design patterns - such as Value Objects and DTOs.

* Anything but very lightweight inheritance hasn't been in favour for many years, and most good OO developers favour composition.

* Writing the simplest version of code for today is a key tenet of TDD as practiced by several OOP leaders such as Bob Martin.

* GOTO is a permanent and nonreturnable change in program flow with little boundaries. Message passing is entirely different, very much bounded, and executed within control flows.

* Poorly designed tests are coupled heavily to code. Good tests are not. Test fakes can actually simplify debugging by removing and isolating large portions of the system.

* Most OO languages have a switch case that's perfectly acceptable to use. Many real-world applications that have never-ending spec changes (compilers work to a pretty limited and well-defined spec) benefit from using polymorphism to allow easier extensibility.

As a paradigm OOP encompasses a particularly wide spectrum, so while you can of course practice the worst OO has to offer in the form of deep inheritance hierarchies and overuse of design patterns "because we'll need them later", none of this is endemic to OO. In fact there's quite a happy medium combining OO with FP concepts (such as React) - or using OO at the boundaries to help assemble and mutate data before it gets passed to a core of pure functions.

As with everything, it's all about picking the right tool for the job, and getting the most out of the tools you are using. Steak knives and bread knives look almost exactly the same, but one is a lot better for tearing through meat.

Historical OOP orthodoxy took great lengths to contrast objects to values. For example, support for values in OOP mainstream languages has been tepid. With Java still failing to fully support value objects at the language level, project Lombok notwithstanding. With Python adding dataclasses support as late as 2017. There is a reason for decades of dragging the foot: OOP orthodoxy shuns values in favor of objects, defined as "identity, [...] state (data) and behavior (code)" [0]. Insisting on "objects" as the only right way to structure programming _is_ the historical failure of OOP. No amount of late attempts at co-opting other paradigms under the OOP umbrella is going to fix that.

I for one welcome the quiet morphing of OOP into VOP/FP. Makes life as a programmer sane again.

[0] https://en.wikipedia.org/wiki/Object_(computer_science)

If you want to understand OOP idea do not think about Java/C# classes and inheritance. Think about OS processes/IPC or microservices. These are Objects. This is the basic idea behind OOP.

Getter/setter is the main anti-pattern of OOP design.

How so?

I think of OOP as a message passing paradigm. It's concerned with how messages are passed from one part of the system to another. It is not particularly concerned with how those messages are implemented under the hood. In that sense it's a higher level paradigm because OOP is all about building abstractions ("objects") and defining how they communicate, rather than wiring code together directly. FP doesn't really have anything to say about how you design your abstractions, just how you implement them in code.

Message passing can be used with a functional language (Erlang) or an imperative language (Go) to great effect. It can also be added onto (as a library) most other languages.

However, I want to know if the original author meant it that way. And I still don't see how message passing is a higher level paradigm than functional programming. It's an orthogonal paradigm, neither subsumes the other, and both benefit when used with the other.

But in practice, does it really make that much difference? A method call is really just a synchronous message. So at that point we're really talking about what messages objects should have - and looking at something like String, Array or Stream in Smalltalk, I don't see how it's substantially different from what we see in mainstream OO languages today.

There is an important distinction. Messages are interpreted, at runtime. Which means you can do certain kinds of metaprogramming without getting outside of the normal tools of the language.

This is not a black-and-white kind of thing, though. A method call can be more or less like a message depending on the language tooling provided.

https://www.baeldung.com/java-dynamic-proxies

C# also has something similar with TransparentProxy, not to mention "dynamic".

>And I still don't see how message passing is a higher level paradigm than functional programming.

Speaking practically, I see a lot of modern technologies that converge (very slowly) on the same ideas Alan Kay was talking about as OOP for the last 40 years. Micro-services, web pages with JavaScript, containers, etc. Those things are pretty high-level.

This seems to be Kay's key point. The description of object orientation is very unlike any modern system I've used, and he mentions elsewhere that even modern Smalltalks fail to live up to it.

My problem with this vision of OOP is that it would seem to take a great deal more support from the programming environment to make it work, compared to FP. Or perhaps the problem is that this "true" OOP is so much harder to grasp that it's impossible for me to approximate it in another language, where with FP I can obtain some of the benefits just by writing pure functions in an otherwise imperative language.

One way to think about this is that there isn't a difference between your programming environment and the rest of your computing environment. There are no real "applications". There are just message sends and objects floating around. This is what Smalltalk was/is like.

You know full well that those founding ideas are mostly irrelevant to what most people mean by "OOP" nowadays. "OOP" right now is C++, Java, C#, Python…

What Alan Kay was talking about is now called the "actor model", of which the most prominent champion is Erlang, which sells itself as a functional language.

Different times, different terms. Which is why I can say with a straight face that OOP sucks and Alan Kay is brilliant.

Design patterns were developed by C++ and Smalltalk people.

The problem of efficiently scaling mountains requires a broader scope. This is why I think formal methods are starting to break into the mainstream: they give us tools to use to simulate and verify designs (model checking, system design validation), validate implementations (verification, proof), and generate provably correct code from high level specifications (synthesis).

Grumpy programmers who think maths is for academics are going to miss out I think. It's an exciting field and the cost for something that used to be only used for extreme circumstances has been coming down so rapidly that it can be effectively used in small businesses as well.

It all comes down to clarity: in communication, in thought, and in practice.

>Whether you use functional programming or dynamic typing it only affects small, local problems in the practice of climbing mountains.

Static typing is a type of formal method.

Of these, only Idris' type system has any power to model truly interesting properties (though the cost of doing so, in program complexity, is huge). Otherwise, even something as simple as rejecting `add(x, y) return x - y;` as a well typed function is beyond all of the others.

As far as ease of use goes, type inference and flow analysis goes a very long way.

>Otherwise, even something as simple as rejecting `add(x, y) return x - y;` as a well typed function is beyond all of the others.

Why shouldn’t that be well typed (unless it is invoked with unsuitable argument types)? Are you saying the language should magically understand the english language meaning of “add”?

Obviously, types and tests help. But it's astonishing how much incidental complexity creeps into one's everyday work with our current tools. Under most circumstances telling a computer to do something shouldn't be that much harder than telling a human to do it (assuming a concrete grammar and shared vocabulary).

In my experience, the compiler is rarely helpful at catching bugs. Most bugs, whether in a dynamic typing language or otherwise, are behavioral bugs that occur at runtime without generating explicit runtime errors, just incorrect but uninterrupted behavior.

I always heard people make grandiose claims about Haskell, like if you get your program to compile, it’s very likely to be correct and run without error. I’ve emphatically never found that to be true.

The types of bugs that compilers can help with are very simplistic most of the time. Requesting a method or attribute that doesn’t exist, typos, confusion about arguments passed to a function.

In dynamic typing, you also solve these same things in a super cheap and low effort way with unit tests.

Additional behavioral unit tests are where real effort becomes required, and these are needed in any paradigm.

Compilers are also not free. My experience with the Scala compiler for example was awful. It is so incredibly slow to compile that I absolutely would rather give up type checking and just use some cheap unit tests to have a much faster development cycle. When you make 1 or 2 small changes and even a smart incremental compiler setup like zinc needs to recompile 30 code units and it takes ~ 3 minutes before you can run tests, this is maddening, and the cycle repeats the whole time you’re working, so it’s this constant extremely disruptive expense.

I’ve had similar thinga happen in legacy code bases with Haskell too.

I’d still much rather have a slightly slow compilation than verify types in my head every time I’m in that area of code, or writing unit tests for every configuration of code which basically just validate I haven’t returned any nulls.

Typed compilation may take time, but it results in faster running programs. And unit tests also take time. I find the errors generated by a type checker come quicker and give more useful diagnostics for deep areas of the code.

Parsing is basically a wash between compilation and interpretation. Dynamic types still need to be resolved for the tests to run. So why would interpretation be faster?

I’m working through a compiler book and would love to know.

It is certainly valuable. A good REPL is completely fantastic for prototyping and debugging. Being able to change how your program works while it's still running and has all its data loaded is great compared to a classic edit-compile-run cycle where you've got to get your program's data re-loaded each time.

But I don't see that this has much to do with compilers versus interpreters, or even really dynamic versus static type checking...

- There are REPL-based environments with integrated compilers, and there are compiled languages with REPLs bolted on top.

- Good REPL support is surely more challenging for languages with strong static typing. After all: what does it mean to redefine a type? what happens to the functions that are using the old definitions? what happens to the instances of that type that are already alive in your program? But these problems all exist in dynamic languages too, it's just easy there to sweep them under the rug by treating them as yet more run-time errors.

For example, I find I am much more productive writing Python code instead of Scala or Haskell, after many years of experience in all three. By “productive” I mean writing fewer defects, completing programs more quickly, and validating that programs are sufficiently correct & efficient for deployment.

A typical work cycle in all 3 languages would be to read code, edit code, invoke a test command from a shell prompt (which triggers incremental re-compilation with Scala and Haskell). In business settings, even for very minor code changes, the incremental re-compilation would take on the order of a few minutes every time, and this was in large companies with sophisticated monorepo tooling and dedicated teams of tooling engineers who worked on performance for incremental compulation. For Python, I just run tests and get immediate feedback without waiting ~3 minutes every time.

The types of correctness verification offered by using the compiled languages and waiting ~3 minutes every cycle was just not useful. I got the same verification in Python by just writing some low effort extra tests one time and then save ~3 minutes on every edit-test cycle.

Haskell let's me encode more of the business logic at the type level. I've finally been able to experience what people mean when they say a type system as good as Haskell's allow you to make sure invalid states are not presentable.

I can do the same in Python, Javascript, etc but it's much more work by writing thousands of lines of test code and still not being certain where the edge cases are.

That's one area a rich type system helps with...

but I think more to the spirit of your comment: it's the behaviors that are most important. No language is sufficiently expressive enough to define what those behaviors should be, and more importantly, which behaviors are not allowed. I totally agree that whether Haskell or Python, when it comes to this problem, neither are effective! There are no compile-time or run-time errors and yet we observe incorrect behavior! That's something I've only seen formal methods able to tackle.

I’ve heard the claim, “Haskell let me encode business logic into the type system” so many times, but I think it’s totally a false promise. Usually people mean design patterns like phantom types and things, and it just leads to the same spaghetti code messes as in any other paradigm.

I’ve never found any cases where encoding this stuff into the type system actually resulted in verifiably more correct code as compared to doing the same thing with analogous patterns in dynamic typing languages and adding lightweight tests. You still end up needing approximately the same amount of test code either way.

Yet in the statically typed case, you often pay a big constant penalty of compile time overhead delaying the work cycle, even for the best incremental compilers.

Well it's working for my code base so it's not a false promise.

I find it hard going back to dynamic languages now because of how little they allow you to see the types.

> I’ve never found any cases where encoding this stuff into the type system actually resulted in verifiably more correct code

I think there is still much debate about this. Dependent type theory is the only type system I know of in which it's possible to write proofs, and therefore verify, a program... but even dependent type theory alone is a bit bothersome for the task.

In my experience it's certainly possible to write a program in Python that is reasonably correct but it takes more effort.

> “In my experience it's certainly possible to write a program in Python that is reasonably correct but it takes more effort.”

I think there is a pivotal trade-off though. I’d argue that in many cases it can be less effort to write correct code in Python for three reasons,

- the simpler types of compiler checks are just inapplicable or handled by totally ignorably-low-effort unit tests in Python and don’t matter 99.9999% of the time, and have low cost in the 0.00001% of the time they do matter.

- the extra type system code and constraints it imposes introduces more extra code than what an analogous set of unit tests would have required for functionally the same level of correctness guarantee in Python.

- the extra time cost of including a compilation step in many edit cycle round trips adds up to far more effort than writing and maintaining extra tests, and disallows flexibly deciding when to get rapid feedback when that feedback matters more than whole-program correctness required by a compiler (and these points are magnified if ever working in a monorepo).

For the last few years I think I've managed to land in the worst of both worlds with SystemVerilog. It manages to combine essentially no type system and no type checking (everything is implicitly just a bunch of bits) with abysmal compile times, so you get neither safety nor a quick turnaround.

All of this makes me really long for both a good type system, and a better edit-test cycle. Which is more valuable? You're probably right. There's nothing more frustrating than waiting 15 minutes to discover a missing comma...

I wouldn't call it "super cheap and low effort", given that tests for stuff like "what if it's not an integer?" tend to be a large part of the overall unit test suite in dynamic languages. Just on the amount of code alone, I would say that it's far less effort to express that kind of stuff in types than in tests.

If you’re testing all kinds of different functions for argument checks or defensive programming conditions, it suggests a refactor to a central sanitizer pattern, and just one small set of sanitization tests. Other functions can take it for granted that the sanitizer works correctly.

You often need the same thing in statically typed systems anyway for cases when calculating whether an input is valid involves conditions not encoded by the type system (possibly even runtime configurable by the user). So except for all but the most trivial kinds of type validation, this does not actually constitute a difference in effort between the two paradigms anyway.

In reality, there are always times where that falls a little flat, which is where IMO Gradual Typing comes into its own. The "core", with some assumptions about the boundaries, be statically analysed. You can add your times(int n) method safe in the knowledge that you'll get a runtime error if someone messes up the dynamic type or doesn't run the analyser.

Ultimately, as I want to run all my code before I put into to production, a lack of runtime errors from my tests tells me my code is correct for the situations I designed it to handle. Now if someone comes along later and manages to invoke a state that I hadn't considered, well... all bets are off.

Terrific metaphor, thank you. I've been stuck with "the map is not the territory" for ages, which is too meta for polite convo.

With "maps / territory", I never thought to ask "do we have to summit the mountain? can we take the valley, the pass? can we tunnel? go around?"

"Grumpy programmers who think maths is for academics are going to miss out"

Probably. I'm still stuck eating the paste, banging the rocks together. Still arguing that Chain of Command is not nested Decorators, trying to explain that memcached (or redis) in parallel vs write thru is a replicant and not a cache, that "agile velocity" means spunk if you're not tracking your defect rate, that Spring & J2EE style DI & IoC is dynamic programming envy (just use Python), etc.

"It all comes down to clarity..."

God help us.

PS- Reading that Twitter thread might be fun, if you have a link handy.

Where I chimed in: https://twitter.com/agentultra/status/1112752548656660482

Formal methods -- or any other useful technique -- are beneficial only once you understand this. Most of the cost is determined by what you build, not how you build it, so the only way to drastically cut it is to build drastically less. Once you've decided what it is that you need to build, you must be ready to pay the cost.

The image I was trying to invoke and the idea implied was that programming languages are insufficiently expressive enough on their own to solve the hard problems in designing systems. They lack the ability to reason abstractly about other processes, agents, and shared state such that they cannot prove anything about their behavior in the context of a larger system. They can't express invariants about the complicated universe of possible behaviors. And the kinds of problems we're tackling today are built on large systems: several interacting processes over an unreliable network working in concert across the globe to keep your data consistent and always available: that's the mountain. Arguing about which programming language or paradigm to use has only a small part to play in the solution to the problem.

https://www.youtube.com/watch?v=tfnldxWlOhM

https://www.youtube.com/watch?v=HnOix9TFy1A

https://pron.github.io/posts/tlaplus-curryon-talk

https://learntla.com/introduction/

https://leanprover.github.io/theorem_proving_in_lean/

https://rise4fun.com/dafny

https://www.betterworldbooks.com/product/detail/Practical-TL...

https://www.betterworldbooks.com/product/detail/Building-Hig...

https://hillelwayne.com/post/pbt-contracts/

[1]: For example, in this case, what you call "a lot" may just be the effect of some sort of enthusiasm that results in publications rather than an actual great number of people. Also, the feeling can be the result of programmers facing an unfamiliar language that is challenging them, hence they are required to focus and think more, and that gives them a feeling that they're writing something that's more correct. That the languages catches early some errors may also strengthen this feeling. They're also likely writing smaller programs. I've programmed in many languages, and one of the languages where I get it right most quickly is assembly, probably because I write smaller things, and because I need to focus much more.

[2]: It's relatively easy to classify which program properties can be assisted by the language and which cannot. Those that can (e.g. memory safety and type safety) are called inductive (or compositional). They can be helpful, but the vast majority of correctness properties aren't inductive. Inductive/compositional means that the property is preserved by all primitive operations in the language.

That's not quite how evidence for the existence of effects works. Evidence for lack of an effect is the attempt, and subsequent failure, to find it.

Few studies have been able to substantiate the hypothesis that homeopathy is very effective, just like the case for FP. It's just that there have been far fewer studies overall testing the second hypothesis than the first. So while we can be more confident that, indeed, homeopathy isn't effective than in the case of FP, there is still no weight to the claim that FP is effective when it comes to correctness.

> there is more evidence pointing that FP leads to correctness than otherwise

There isn't.

It's perfectly OK that people write about how much they like FP or OOP because the paradigm fits well with how they think, they like its aesthetics, or any similar reasons. It's not OK to try and justify the preference by making up completely unsupported empirical claims.

And by the way, even when there is no evidence one way or the other, you still cannot claim there is an effect.

> There isn't.

But there is. Take this paper for example, http://web.cs.ucdavis.edu/~filkov/papers/lang_github.pdf "A Large Scale Study of Programming Languages and Code Quality in Github".

"The data indicates functional languages are better than procedural languages; it suggests that strong typing is better than weak typing; that static typing is better than dynamic; and that managed memory usage is better than un- managed. Further, that the defect proneness of languages in general is not associated with software domains. Also, languages are more related to individual bug categories than bugs overall."

1. Found a statistically significant, but a rather small effect (low single digit % IIRC) that cannot justify language/paradigm choice (choose FP for 1.5% fewer bugs!). If anything, it's evidence against a large effect.

2. Had most of even that small effect disappear on reproduction, which increases the evidence against a large effect: https://arxiv.org/abs/1901.10220

There are typed and untyped languages in both paradigms. There actually have been a couple of studies that found a positive effect for types on correctness. The largest effect (15%!) was reported in this paper: http://earlbarr.com/publications/typestudy.pdf but it compared only TypeScript and JavaScript.

2. Why the different category? Both effects were looked for and not found. Homeopathy was just looked for much more, so the certainty it has no effect (beyond placebo) is more certain. Again, the effect of FP on correctness is currently between completely unknown and some evidence against. Repeating this claim without supporting evidence is ridiculous.

> Explaining why it is unlikely (from a theory perspective) that languages like Haskell have a significant effect on correctness is easier [2]

> It's relatively easy to classify which program properties can be assisted by the language and which cannot. Those that can (e.g. memory safety and type safety) are called inductive (or compositional). They can be helpful, but the vast majority of correctness properties aren't inductive. Inductive/compositional means that the property is preserved by all primitive operations in the language.

2. Because homeopathy's claims and method of action can be dismissed a priori, due to the fact that they don't follow the laws of nature or the chemical principles of solvation.

Further, your are conflating the question " could (typed) FP be use for correctness" with " should (typed) FP be use for correctness", and while the answer to the first one is trivially "yes", you appear to be chasing the answer you want ("no") to the second question. This puts your approach closer to that of the homeopaths.

> your are conflating the question " could (typed) FP be use for correctness" with " should (typed) FP be use for correctness", and while the answer to the first one is trivially "yes", you appear to be chasing the answer you want ("no") to the second question.

I am not conflating anything, and I certainly didn't say which programming paradigm people should or shouldn't use. I did say that if people care about correctness, they should look elsewhere than to change their preferred paradigm to or from FP, and focus on techniques that seem to have an actual effect on correctness (BTW, switching languages -- among several reasonable choices -- is often costly, and language in general is one of the choices with the least drastic effect on most important software metrics, except maybe when it comes to performance, where most of the time what matters is the runtime, and not so much the programming paradigm).

BTW, while I won't get into the discussion about types (which, again, is complicated, as there are different kind of types and usage of types, each with very different cost/benefit), the largest effect types -- and language choice in general -- have on correctness was found in a study I linked in another comment to be of 15% (in bug reduction), when comparing TypeScript and JavaScript. In contrast, several studies and case studies have found code reviews to have an average effect of ~60%. So the largest effect language choice was ever found to have in a single study is 4x smaller than the effect of techniques that are far cheaper than a language change (well, maybe not in the case of TypeScript/JavaScript). Really, language is one of the costliest and least impactful factors on correctness (except maybe when the language is unsafe).

In summary, no connection between FP and correctness has been established, period (and what little evidence we have seems to suggest there is none). People should use whatever paradigm/language they like; the chosen paradigm doesn't seem to have a large positive or a negative effect on correctness. People shouldn't make empirical claims that are unsubstantiated.

> Because homeopathy's claims and method of action can be dismissed a priori, due to the fact that they don't follow the laws of nature or the chemical principles of solvation.

I wasn't trying to say that people who believe FP has an effect on correctness are exactly the same as those who believe in the effectiveness of homeopathy. I only said that the fact that some people make the claim enthusiastically in blog posts should not be taken as corroboration to its validity, just as the number of enthusiastic posts about homeopathy is not evidence in its favor. People often enthusiastically believe things that aren't true because personal experience can be misleading.

But anyway, the claim that FP improves correctness similarly does not follow any law of software correctness. If either homeopathy or FP were to have an effect, it would have to be through some as-of-yet undiscovered process. As any program could be mechanically translated between pure-FP and imperative, there is simply no CS theory to explain why FP would have an effect on correctness (as opposed to, say, using a model checker), and there is no such programming-process theory, either (as opposed to, say, code reviews).

Thank you, that's what I meant.

> The claim that FP improves correctness similarly does not follow any law of software correctness. If either homeopathy or FP were to have an effect, it would have to be through some as-of-yet undiscovered process.

Again you are conflating could and should. Let's simplify:

Homeopathy CANNOT be used, since the concept fundamentally don't work and hence SHOULD not be used.

FP for correctness CAN be used, since we do have examples of functional languages that can be used with formal verification tools, type-based or otherwise. Whether it SHOULD be used, does not follow from whether it CAN/CANNOT be used. That's a question for the sociology of software engineering, and like you say, that's complex.

>People should use whatever paradigm/language they like

I agree, which is why I dislike when people try to associate certain preferences with pseudoscience.

You hit the nail on the head:

The Safyness of Static Typing

https://blog.metaobject.com/2014/06/the-safyness-of-static-t...

(This is obviously for static typing, not FP, but the mechanism appears largely the same and the overlap is substantial)

Now, CompCert was verified using deductive proofs. In industry, this is an approach that's hardly used (in part, CompCert was done to show that it could be used at all, at least in principle). Verification in industry is normally done using model checkers, that are fully automated. There are tradeoffs between deductive proofs and model checkers (and sometimes deductive proofs are used to close some holes left by model checkers, or tie together some modules verified by model chekcers [2]), but they scale better. Model checkers used in industry include Spin[3], nuSMV[4] and others.

So model checkers check software that's larger than CompCert every day, but they don't get papers written about them, because their use is more mundane than heroic. They are also used for imperative languages, because formal verification of functional programs is behind (here is Simon Peyton Jones saying that [5]). Model checking functional languages is hard, because higher-order functions are hard to verify. Instead, there are model checkers for C, Java, hardware definition languages and tool-specific languages.

So, this mentions a 1MLOC Java application by Fujitsu that's been model checked[6] with NASA's Java model checker (that's 10x bigger than CompCert), and here's a report about model checking a many small C programs[7]. Again, software verification of imperative languages is almost mundane; what you read about are exceptional things.

Also, people who are interested in programming languages are normally introduced to formal methods through its small intersection with programming language theory, and that intersection includes uses of proof assistants and dependent types. Because functional languages are liked by language theorists (for many reasons I won't go into), then that's what you see. But that is a very small part of formal methods research. Most of it is research into model checking and sound static analysis, and most of that work is done in imperative languages. Not because they're easier to verify (both functional and imperative are just as hard, but pose different challenges), but because they want to check programs in languages many people use, and language doesn't make much of a difference.

Finally, I should add that even though language doesn't have a huge impact (there can be some exceptions; e.g. unsafe languages such as C do add some challenges), there are languages that are more natural for verification; they are not functional or classically imperative, though, as those two are both mediocre. Rather, those languages are synchronous languages (usually imperative, but not like what you're used to). Normally, those languages are used in hardware and real-time software (Esterel[8], SCADE[9], but they are now starting to make their way into the mainstream with Céu[10], "behavioral programming" in JavaScript [11], and, perhaps most famously, with Eve [12] (RIP). To see why these synchronous (but imperative) languages are a good fit for verification, take a look at how easy it is to specify a correctness property in Eve: [13].

Finally, my own favorite specification and verification language is TLA+ [14], which is neither functional nor imperative (but it is synchronous; then again, it's not a programming language), has been used to verify very large programs at Amazon and elsewhere [15].

To get back to where I started, CompCert (and seL4) are not really examples of anything. They were both huge, heroic efforts (that didn't quite prove as much as you think they did) by academics in the lab on quite tiny programs. While these efforts are important for some niches, you can't generalize, just as you can't generalize from the design of particle accelerators used to turn some lead atoms into gold atoms to learn about how best to design metalworking tools. Full, end-to-end verification, is something that we simply aren't yet capable of doing in any generalizable or scalable way, regardless of language.

Real-world verification efforts are quite different, and are done with imperative languages both because that's what people use and the language doesn't have a big impact, and becuase there are still issues with model checking functional programming languages.

[1]: http://video.upmc.fr/differe.php?collec=S_C_colloquium_lip6_...

[2]: http://events.inf.ed.ac.uk/Milner2012/J_Harrison-html5-mp4.h...

[3]: http://spinroot.com/spin/whatispin.html

[4]: http://nusmv.fbk.eu/

[5]: http://events.inf.ed.ac.uk/Milner2012/Monday_Panel-html5-mp4...

[6]: http://javapathfinder.sourceforge.net/events/JPF-workshop-05...

[7]: http://www.csl.sri.com/users/ddean/papers/ndss04.pdf

[8]: https://en.wikipedia.org/wiki/Esterel

[9]: http://www.esterel-technologies.com/products/scade-suite/

[10]: http://ceu-lang.org/

[11]: https://youtu.be/PW8VdWA0UcA , https://vimeo.com/298554103

[12]: http://witheve.com/

[13]: http://witheve.com/#correct

[14]: https://lamport.azurewebsites.net/tla/tla.html

[15]: https://lamport.azurewebsites.net/tla/industrial-use.html

What about user interfaces? What is a "correct" user interface? If a bug is "unexpected" behavior, and my user interface has several thousand users, how do I manage to not produce unexpected behavior to anybody?

Many software supports workflows and processes in some enterprise, and those workflows shift subtly over time. How does Haskell help me write "correct" software in such a context, whatever that means?

How do I deal with low quality of input data, when I can't ask my product owner to create a matrix of each case of missing data and behavior, because that would be exponential in size?

Phrased another way, the problems with correctness that seem to trouble the author are not the problems with correctness that I tend to encounter often in my work.

The case where there is a clear-cut bug in an algorithm tend to be easier to debug and fix than a bug that stems from several department having subtly different ideas of what certain pieces of data and action mean.

Could you, or should you, use formal methods for everything? No. But it can be applied pretty broadly if you're open to it, and in fairly lightweight ways (especially these days since there's been a ton of interest over the last few years).

Once you start recording your formal (or more formal) specs, you can also share them more easily. A major problem in coordinating with so many different groups is that they all have their own model for what's going on based on their interaction with the systems. By creating more formalized models that allow for clearer communication (a few statecharts versus pages and pages of prose; flow charts versus pseudocode) you can reduce the communication error between teams/departments. And with all the recent work going into it, and using more capable languages (or tools with less capable languages) you can encode much of this into your program and make correct system construction more feasible.

[0] https://sketch.systems/

The thing is, I've come to the opposite conclusion.

My conclusion is that programmers have been trained to think about correctness. What they should be trained on and design is to account for inevitable failures. My main paradigm is the floating point design. It incorporates a built-in invalid value, which neatly propagates itself. Objective-C also has this concept of propagating a chain of failures accross function calls.

Your programs will be buggy, your data will be wrong. Design to support propagating it with null actions and detect it at the top of your action loop.

(One of the unfortunate heritage of computin ghistory is the missed opportunity of the binary system imbalance around zero. Both 1-complement and 2-complement have abnormal values. In 1-comp, it's negative zero. In 2-comp, it's the fact that the most negative number has no positive value and is its own negation (- INT_MIn == INT_MIN). It was an opportunity to reserve such value for invalid integers. Then you design your null pointer to be that value too, and NAN to be that bit pattern. Than all your fundamental invalid values map to the same bit pattern that can easily be propagated. Oh well.)

That is pretty much the design philosophy of Erlang. You should check it out if you haven't.

It could be argued that all engineering problems _are_ economic problems.

(1) Specification (2) Implementation

Specification has always been the primary problem, the simple reason being that we are trying to quantify human desires regarding information flow. As we are finding out, it's non-trivial to say the least.

This goes back to an earlier talk I learned about here and watched just this morning by the outstanding MIT professor Nancy Leveson, https://www.youtube.com/watch?v=WBktiCyPLo4, who has analyzed various engineering problems (including the Challenger disaster) and even published an entirely new methodology for analyzing large-scale systems. Her book can be downloaded for free at http://sunnyday.mit.edu/safer-world.pdf.

Of course, economics factors into everything people endeavor to do these days, but strictly within the domain of creating correct information management systems -- from a purely technical level -- the problems are specification and implementation, in that order. Getting someone to pay for the time and team needed to do the job correctly is a completely different story, and not a pleasant one, it seems.

Namely, is crappy software actually more efficient? Does it deliver more value for less cost? Or is it, instead, that crappy software is a bad value, but markets are not transparent enough, and it is too hard for clients to assess whether the software they have received is crappy and too hard for businesses to convince people to pay them for quality?

If you hire a maid who always manages to miss a spot or two cleaning your bathroom, does it really matter? Your bathroom is a lot cleaner than it would've been otherwise, so mission accomplished in the grand scheme of things.

On the other hand, if you hire a mechanic to overhaul your car engine, you might not be able to tell the difference when you drive it home from the repair shop, but if they did a poor quality job, it is going to come back to bite you. Quality is important even if you need to pay more to get it.

Which one of these two things is software more like? I could see it going either way. Maybe it depends. Maybe there are ways you can cut corners that are a win (more value / less cost) and other ways that are a loss.

It depends on the spot missed: is it contaminated with fecal matter? There you get into the realm of risk management. The problem is that, with software, one bad mistake can leave the user with complete loss of data. Look at Microsoft's recent update debacle; some people lost a great deal of data.

>> Namely, is crappy software actually more efficient?

Never. As the Chinese expression goes: Pay a lot, cry once.

The problem is that the people who pay for the creation of software (i.e. corporate directors) are usually ignorant about all things except for money and the vague desires of their customers. The folks that can specify and implement the systems rarely have the clout to allocate the resources necessary to get the job done well.

>> Which one of these two things is software more like?

Information systems (software that must run over and over again against the same data, often concurrently) are actually engines in that they must withstand stopping and starting; of course, the information engines that run continuously are even more difficult to keep functioning as their uptime stretches on. Therefore, the answer to your question is that software is most certainly more like an engine because information systems are engines, just that their fuel is data (including user input) and their output is information (data made meaningful to human beings) and changes to its information base.

We can all see how the poorly designed information engines of the world accrue ugly cruft that eventually leads to their needing to be "re-built", which, for example for Windows, means re-installing from scratch.

Unfortunately, I don't see either side backing it up with anything that looks like real evidence. It's so complicated to evaluate that I don't think anyone really can prove either way. But you can't not have an opinion since it's an important question, so it seems like people join one camp or the other mostly because it suits their personality or working style.

If they take pride in their work and feel disappointment at the prospect of producing code they can't be proud of, they tend to believe quality is worth it in the end. If they are impatient and like to wrap up one thing quickly so they can move on to the next thing, they tend to be in the other camp.

I myself am in the quality and correctness camp, and I really would love to know that it always pays off because that would mean the way I prefer to develop software is also the most practical and reasonable way. But I can't really prove that it's the right view when you consider the economics.

Oversimplification. Solving a problem just well-enough to live to fight another day is baked into capitalism in a deep way through competition, whether that competition is internal or external. .

I have many many examples from real life, for instance, one from banking; sometimes I have to work with systems that are responsible for 100s of millions of $ in transactions that are just ductaped heaps of crap. They are running on many servers because they continuesly crash and mess things up (literally corrupt data which has to be manually fixed).

The software was written by juniors with a lead tech who only made some web scripts before and all was hurried to the 'finish line' to get more investment.

All of these decision where economic; hire cheap people to show bums on seats, hire cheap management because good management costs a lot keep pushing for deployments even though everything is ill tested because the need for more money.

The result is that the entire team is all day (and night) busy putting out random appearing fires and the average period for an employee to stay is 6 months after which the stress catches up.

Ofcourse they still are doing really well as these type of companies are experts at hiding things like this. Thick rows of sales and account management people to hide the poor execution. Reminds me of IBM in the 80-90s; slick looking suits and shiny boxes but the software they shipped was just pure vomit; it still sold fine (not sure if it changed; I have not worked with them anymore).

Obviously they would be really raking it in if there weren't 40 people 24/7 trying to keep the stuff on the servers from completely exploding.

After a week of hard work in these kind of circumstances, I always enjoy reading HN + Reddit in the weekend and seeing these wide eyed youngsters here thinking that every company does code reviews, unit tests, uses versioning tools (...), not using php for near real time banking backend banking transaction applications (...), kubernetes/docker, microservices, serverless software while in reality it is a microscopic % and very large numbers of money is still being earned through absolute software poop.

Right now there is no reason to think games will even need that level.

I haven't seen this yet, but I sure hope to. I'm stuck in the "everyone does devops now" paradigm :(

But it helps to eliminate large classes of bugs where you can, so you can concentrate on other things.

As an example, if you try to write our own web search engine, the linear algebra or neural network operations you may be using are certainly amenable to mathematical reasoning, but the relevancy of the returned results is not something you can prove mathematically.

And in my opinion, this fact often leads "correctness" fanatics to retreat to safe areas where their methods work, and snipe at all the rest of the world. Characteristically, the article quotes E.W.Dijkstra, whose much beloved notes are full of explorations of mathematical toy problems, and catty dismissals of anybody trying to make real world use of computers.

When Knuth was dissatisfied with the results of early computer typesetting, he spent years of his life developing TeX. Meanwhile, Dijkstra kept hand writing his papers and having staff turn them into printed form. That, to me, is the epitome of the "correctness über alles" mindset.

I think it'd do you some good to read a bit more of his work and the history of computing.

Yes, Dijkstra made major contributions to algorithms—exactly the "safe corner" where correctness thinking applies. Ironically, one of his contributions was to the concept of semaphores. I sure don't hear any of Dijkstra's fans claim today that if distributed programs just used semaphores, all our concurrency problems would be solved.

Another important contribution: The Banker's algorithm, of which Andrew Tanenbaum observed (Modern Operating Systems, 2nd ed):

> The banker’s algorithm was first published by Dijkstra in 1965. Since that time, nearly every book on operating systems has described it in detail. Innumerable papers have been written about various aspects of it. Unfortunately, few authors have had the audacity to point out that although in theory the algorithm is wonderful, in practice it is essentially useless because processes rarely know in advance what their maximum resource needs will be. In addition, the number of processes is not fixed, but dynamically varying as new users log in and out. Furthermore, resources that were thought to be available can suddenly vanish (tape drives can break). Thus in practice, few, if any, existing systems use the banker’s algorithm for avoiding deadlocks.

... which is pretty much my argument: Dijkstra picked himself the neat little corner that WAS amenable to mathematical reasoning, at the expense of real world applicability.

One of Dijkstra's contributions to language design was resigning from the Algol 68 committee. It might do proponents of formal methods good to reflect on why that language was less than a stellar success, given how strongly it relied on advanced formal descriptions.

But the question is not whether Dijkstra contributed to algorithms, language design, or concurrent+distributed computing (he certainly did). The thesis that the Article presents (and supports by quoting Dijkstra, who did agree with that thesis) is that formal methods apply universally in system design, and that today's software woes are largely the result of insufficient application of formal methods.

It is there that I disagree, and that Dijkstra kept pontificating about despite having abolished programming and using computers around the time he started focusing on formal methods. And that detachment from and disdain of the actual practice of computer use is what renders his later opinions suspect to me.

Within corporate environments, the ultimate problem is that the people who allocate the resources are usually the least knowledgeable about the costs of "digging a hole" (i.e. technical debt).

Of course, there is a great deal of blame to be placed on our -- the developers' -- shoulders, but guesstimating software delivery is difficult enough without non-technical people setting ridiculous timelines. I'd say the solution to the problem is to have managers select competent, driven developers who care about quality, and then for those managers to trust the technical teams to get the job done right. For such a team to work, each piece must work well and work hard.

Two quibbles: Haskell is prone to something that might be considered a class of bug that Rust avoid: the space and time performance of idiomatic Haskell code can be very surprising.

I also wonder at the possible answers you give to " “When” would you say that the software had a bug?" - the most obvious answer to me is when the commit is made to the codebase that introduces possibly observable incorrect behaviour.

My point is that I actually think that Idris could end up being successful in an industrial sense, due to the fact that it gives you all the correctness guarantees of Haskell (and more), but has managed to (thus far) avoid a lot of the cruft that has built up in the ~30 years Haskell has been around. Fingers crossed.

[1] http://docs.idris-lang.org/en/latest/reference/uniqueness-ty...

Rust's advantage is that its borrow system, with reborrowing rules and such, feels much more ergonomic.

If I knew anything about elaborate type systems, I would try and address your complaints. Sadly, my knowledge of linear logic and whatnot is very ad hoc.

The fact is that, for the vast majority of workloads, which are not heavily algorithm dependent, idiomatic Haskell is going to be much faster than what most people are using. For the algorithm dependent ones, a Haskell programmer familiar with GHC's optimization layer should suffice to get very good performance. I've written several high performance Haskell programs, and it's moderately time consuming but not anymore difficult than other languages.

I am not trying to be pedantic, but your point is moot if you consider what "most people" are using are not dynamically typed interpreted languages like Python Ruby or PHP, but rather statically typed, compiled languages like Java, C#, and C++. Java by itself dwarfs Python and Ruby combined.

Here are some benchmarks: https://github.com/jakubkulhan/hit-server-bench. As you can see, warp is on par, if not better than, many of the common JVM based options.

I'm not arguing Haskell is necessarily better than Java in all benchmarks (or C#). Merely that IME, most people dismiss Haskell as slow because it's a functional language, despite increasing evidence to the contrary. It is certainly capable of standing on its own against popular languages.

To your second point, I think the author is making an argument that it can perhaps even be earlier than that: the bug is introduced when the programmer's model of the behavior differs from reality. That is to say, the "bug" exists purely in the developer's mind. After that it's a matter of course for the bug to be transferred from there to the codebase.

If the developer chooses to interrogate their model before committing it to code, there is the possibility of the bug being caught before it ever makes it into the codebase. But perhaps it is still correct to say the bug still existed, for a short time, at least.

That is indeed one of Haskell’s drawbacks, though personally it’s one I am comfortable with given the alternatives. I’m happy for a program to be correct and less performant than fast and wrong. The performance issues are also not intractable. The tools for measuring this are pretty good.

For example, due to laziness, file-streaming with lazy IO can end up with files being closed before you're done consuming. This is almost certainly never what you want, so Haskell's system actually hurt correctness.

In that particular case it's easy to get around if you use the Conduit library, but that's just one example.

I will say that personally I have become somewhat enamored with Idris, but I think that most of the people that work on it claim that it is not production ready, and I've not used it for anything but personal projects. Still, I love that it gives me everything that I like about Haskell, and it's young enough to not have many of the drawbacks, at least not yet.

   ReasonML - OCaml - https://reasonml.github.io
   PureScript - Haskell - http://www.purescript.org
   TypeScript - https://www.typescriptlang.org
   Scala.js - http://scala-js.org
   Elm - https://elm-lang.org
   ghcjs - Haskell (https://github.com/ghcjs/ghcjs)

http://bikeshed.fm/192

My (now former) boss was non-technical. Wondering if anyone else has encountered such a person? Coming from other industries, is it common that people view software engineers as somehow sloppy or lazy in their work? Is it really true? Is it unreasonable to expect a competent engineer produce working, correct & bugfree performant code on the first try? I’ve definitely had my moments of brilliance where it all “just worked” but that usually isn’t the case and I’m wondering if it could be something wrong with me?

So, no, like life itself, we all make mistakes in our systems. The important thing is that we don't make the same ones over and over again. In software development, that means adjusting our development methology to make such bugs less likely in the future. That is why software development is both the most challenging and most rewarding of careers. Of course, I may be a bit biased ;-)

As far as encountering crappy managers, I'll just say that I can count the good managers I've had on one hand and still have a couple of fingers left over. As to your former manager's particular flavor of belligerence, I haven't had that one specifically, but there are very much uglier variants, my friend. My understanding is that one cannot be made a manager unless the person is willing to prioritize money over human beings and it doesn't take a biblical scholar to see how that is causing so many problems in the small and large across the world. In the small, that attitude manifests itself in many ugly personality traits, while being the foundation of the entire structure and intention of the for-profit corporation where the vast majority of us are forced to find our work.

The same thing goes for the industry - I think that it's accurate to describe modern software engineering as "sloppy", in general, especially if you compare it to the standards in engineering proper. But we're there because this is what the market is willing to pay for. Much like all the people complaining about all the cheap Chinese junk in stores, but not willing to pay significantly more for quality.

My take on correctness is this: for ethical reasons, a developer should never be the final say on whether their solution is correct.

The users, whose voices are concentrated in the one and only Product Owner, should always have the final say on the correctness of our production code.

The tricky bit is proving to the Product Owner and ourselves that we have met the users' expectations.

I believe this is where testing and refactoring comes in. Language and programming paradigm choices are window dressing if the actual code is a slapdash mess with no formal proofs of correctness.

Until some genius comes up with something better, those proofs must take the form of fully passing, comprehensive test suites.

The only mindset required to avoid long-term bugs and maintenance problems is a personal conscientiousness, a personal approach to defensive programming based on (ideally, extensive) personal experience, which will inevitably include a very-hard-earned skillset of decoupling.

Everything else is trivial (borderline bike-shedding) in comparison.

Static types, OO, functional programming, agile, TDD, etc, etc -- these will not save you from your own personal deficiencies. Only long, hard practice will.

A skilled practitioner can build a large, complex system in Visual Basic or PHP using entirely OO idioms. Now he or she may do a somewhat quicker (and happier) job if he or she is able to employ some convenient tools of the trade (eg syntactic niceties, functional-orientation, immutable libs, testing libs, etc etc etc). But the quality and manageability of the system is entirely a function of experience-based skillsets that far transcend the particulars of the programming paradigms that we currently have available to us.

I've seen many a strong static typer, who thinks they have found God, make an absolute mess of everything including its leverage of the type system over time.

I've seen many a developer write OO code within a functional language and vice versa and the success or failure in these cases is irregardless of even the slight misapplication of the tool in hand.

Can you articulate a real world problem into a sound domain model? Can you decouple the behaviors of your system into composable parts? Are you conscientious enough to informally "prove" the transformations (ie git commits) you make to your software system?

If you can do these things, you avoid a mess of a system regardless of your PL and programming paradigms.

If you cannot do these things then no matter what kind of process you bring to the table, you will not be saved.

The first thing that comes to mind is Gary Bernhardt's talk on Boundaries, or "functional core, imperative shell", but I'm not sure that this is entirely what you're discussing here.

Most writing on software of course is technical (on PLs, algorithms, processes) but there seems to be very little to guide the software practitioner who really wants to seek mastery.

> what resources or heuristics or strategies would you suggest to help draw the lines between behaviours or modules?

The best I can come up with for teaching this would be to create some concrete "problems"/scenarios that would exercise the skill set, and then reveal various ways the problem could be decomposed and quantify the degree of decoupling and even reveal the practical consequence of the coupling by introducing new "requirements"/dimensions to the scenario.

I appreciate that in some cases the specification is straightforward and the challenge is to implement it correctly. But I think in most software development it is really the other way around: Designing/specifying the expected behavior is the hard part. It is pretty straightforward to implement this behavior correctly.

It follows that as commonly used the term bug refers to a pleasantness defect rather than a correctness defect. And this stands up to our day to day experience. In the overwhelming majority of cases users report bugs because they are displeased by a behavior, not because they studied the specification and discovered a correctness error.

On a more serious note: the biggest barrier to correctness I've encountered is doing things I don't understand. I also care less and less for being paid to understand particular things, it's so much worse than just being paid to do work.

This one is particularly obnoxious because he's aware of the tribalism and thinks that by mentioning it then his post is magically no longer merely more fuel to the decades-old flamewars.

You will always run into issues because code just like matter decays to entropy.