[tyu2]

From one perspective types (and I mean proofs encoded in types) is a compile time measure against bugs, while supervisors is a runtime measure. It's much easier and more productive to not do proofs and rely on runtime architecture for reliability, it adds relatively little complexity and asks very little from developers, it stays almost the same as regular software development. And it's still necessary to do regardless whether you have proofs or not.

And types like machine types are of course irrelevant for BEAM, well, maybe they'll start to matter a bit with JIT, but probably still not, BEAM with JIT is still not going to be a performance miracle.

[ProfHewitt]

Strong types are very important for concurrency.

However, by themselves, strong types do not provide proofs.

See the following for proofs of strongly-typed concurrent systems:

https://papers.ssrn.com/abstract=3418003

Strongly-typed programming languages need to provide

additional capabilities for error processing and recovery.

[jpcooper]

Thanks for posting. I can't find it now, but we mention somewhere in the paper that typing makes it more difficult to fake messages. Typing allows you to make stronger proofs over the properties and behaviour of actor systems. Sorry if I've missed the point: What are the other direct implications to security which typing brings?

[ProfHewitt]

Excellent question! Types can provide very strong security

for messages by having the type system do crypto so that

applications can benefit without requiring application

programmers to manage keys and crypto code.

[jpcooper]

Thanks. That makes sense.

[ProfHewitt]

You are very welcome.

There is additional information available here:

https://professorhewitt.blogspot.com/

[jpcooper]

Without trying to sound too flamebaity, as typed versus untyped has been discussed endlessly, I would like to see a study which compares development time and reliability between a Erlang and another typed language running on BEAM. That is, typed versus untyped for the sort of systems which are built with Erlang.

[lostcolony]

So I can say from experience, none of the production issues we ran into in two and a half years of Erlang would have been solved by better typing.

That said, our own practices meant we included a lot of unit and API level tests, and some of the issues I personally caught and fixed when testing might have been avoided by typing, and were, eventually, when we added Dialyzer about a year and a half into the project.

Dialyzer itself was worth it to me only insofar as type specs gave me a language to express the typing I was going for, rather than leaving it implicit. It also helped me understand what my colleagues were trying to do in some cases. The explicitness helped me feel better about what I was doing as well; in hindsight I don't think it sped up development, nor did it reduce bugs (though it likely reduced testing time...but that's probably a wash given the time to get the spec right, and update it as data structures evolved).

Can't speak to using another language on the BEAM, whose typing isn't optimistic like Dialyzer, but my experience with Dialyzer, at least, left me feeling subjectively better about the code, but objectively and in hindsight I don't feel it gave us measurable improvement. Just more confidence. Which may be enough of a gain; confidence in the system is what you want when you're optimizing for reliability, even if it's not really a gain on that front.

[jpcooper]

After years of using statically type checked languages like Haskell, I’ve observed that I am quite lazy. If I went to a language without static type checking today, I wouldn’t trust myself to provide the right function arguments in the right order all the time, or to send the right message types, especially after refactoring. It would be a nightmare for me to have to write unit tests for this. Maybe that would improve over time, or maybe I’m just a crap programmer.

[lostcolony]

Well, as strong a type system as Haskell likely prevents enough bugs in the code to let you feel safe without unit tests. That's what I'm talking about; that -feeling- of safety.

Do any of these languages help prevent you from writing code that simply does the wrong thing? No. You multiplied instead of adding; no static type checker is going to catch that, because you semantically told the computer to do the wrong thing.

That's why I wrote extensive tests; I needed to make sure the code did the right thing, reliably. It's also why we chose Erlang; supervisor trees and immutability meant that as long as we tested and felt good about the happy path, the unhappy paths would generally take care of themselves.

As an aside, in Haskell, you actively have to make tradeoffs around laziness, too. Both these data types are Integer -> I either have to create a custom data type to distinguish them (increasing level of effort as a dev), or I risk getting them in the wrong order if they're both passed into the same function. Named parameters might be a better solution here, and that can be done regardless of typing.

[jpcooper]

Yes. I agree that you certainly need to write tests for algorithmic code unless you are formally proving it. I definitely would not feel safe about a data structure I wrote in Haskell without writing a large suite of tests. If your tests cover a good portion of the code, then errors arising from incorrect arguments will be quickly found. It's nice to have that eliminated by the compiler when possible though.