Why Don't People Use Formal Methods?

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

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.

I suspect it’s this: Z notation

1 Like