Although not a formal formal method type driven design with F# or Haskell is something to look into as well. Here your axioms and code blend together and you are relying on the language compiler to model check for you.
1 Like
Can you give links to your preferred reading material for that Z thing, please?
Truthfully, after all the reading that Iāve done on the subject in the last few years, I have come to believe the static (and strong) typing systems are the lowest hanging fruit when it comes to tightening the grip on your code and demanding a class of bugs be eliminated from it by the mere virtue of it compiling at all.
On that lane of thought, Go seems to do poorly, Rust is okay-to-pretty-good, and OCaml and Haskell seem excellent. Stuff like Alloy and Idris are way too specialized for me.
Of all these, Iām only inclined to pick OCaml so far. Itās concise, has lightning-fast compiler, the syntax is actually quite intuitive, and itās endlessly expandable due to metaprogramming and DSL creation being very easy and standardized.
I quite love Elixir and this will not change but itās an uphill battle to make it as safe as a strongly and statically typed language. Oh well, I still love it.
3 Likes
Well, erlang was developed to be extremely resilient against any failure, not just type failures. In addition it was developed with massive code bases in mind. Something people claim dynamic languages canāt handle.
I think erlang is safer to run than most statically typed language. Formal verification may be a way to actually change this but as with everything there is a cost involved.
The standard type systems such as go, java and C donāt give you enough safety at all.
And even with a stronger type system I am also not sure the class of bugs eliminated from a static type system is good enough. Because often they believe the type system is enough to prevent crashes whilst in the real world it is not.
Also, type system do not work well together with the real world where external components donāt cooperate and change contracts, throw random errors and in other ways misbehave. This is where the BEAM concept of error handling shines. Because it understands these things happen no matter what your type system says.
2 Likes
Iāve never used F# and maybe never will but I find myself on https://fsharpforfunandprofit.com/ all the time.
1 Like
Although I started from the same premise, (might explain why I keep going back to relearning Haskell every few years), my experiences with Erlang/Elixir projects have changed some of these thoughts.
In particular by splitting the project into applications with smallish GenServer/GenStateMachine I found the majority of defects are either code trivial or system related.
Code trivial tend to be missing a pattern match in a function header related. This is the most common variety.
System related would be hard for any method to catch. Usually related to slow network, slow disc drives, misconfigured routers etc.
2 Likes
You can get answers to your questions in a link provided here: https://twitter.com/lemmster/status/1111068407934312448
And ābeginners questions welcomeā is explicitly stated.
There you are thank you youāre welcome. 
Hillel heeft geretweet
lemmster ā @ lemmster 15 u15 uur geleden
Meer
Als antwoord op @ hillelogram @ Apress
I donāt understand why everybody is afraid to post to the Google group. Why wouldnāt we want beginner questions?! What can we do to remove this impression because this community segregation is IMHO much more harmful than beginner questions on the group?
In my experience, inadequate type systems like those in Go, Java, C++ eliminate the classes of bugs that are trivial to debug, while doing nothing to reduce the hard-to-debug concurrent stuff. Elixir makes it easier to write reliable concurrent code. Rustās type system has that as an explicit goal, and though Iām beginning to work with it, I canāt comment yet on how successful I think it is. Haskell & OCAML I canāt really speak toā¦
1 Like
Hi,
Could you please elaborate a bit more on the āBEAM conceptā? What do you mean? Is there more documentation available?
Cheers,
Marcin
With the BEAM concept I guess I mean the notion that each process runs in isolation and is not handing its own errors. You can then link processes and monitor processes to handle errors at another place.
For this to work you generally write the āhappy pathā and only deal with errors which are part of your business logic and if anything else happen you ālet it crashā. This is basically the complete opposite of strong typing systems where the type system in many cases force you to handle all errors here and now. Ocaml, rust and haskell has exhaustive pattern matching meaning that you must match all possible return values from a function whereas in erlang/elixir you are encouraged to only match what you need.
Both ways try to eliminate bugs. One by forcing you to deal with all variants even if you do not care about them and do not know how to handle them. One by handling only the variants you want and letting the process crash if you donāt handle a scenario.
For a better description Iād suggest this article and talk:
5 Likes
Thank you very much @cmkarlsson for the explanation and the links. This is a good material to go through.
