# On "Why Elixir?"

**URL:** <https://forum.elixirforum.com/t/on-why-elixir/34038>\
**Category:** Discussions\
**Tags:** releases, elixir\
**Created:** [August 27, 2020, 7:03pm UTC](https://forum.elixirforum.com/t/on-why-elixir/34038 "2020-08-27T19:03:55Z")\
**Posts on this page:** 1\
**Showing post:** 2

<div class="post-metadata">

**Author:** ![krstfk](https://forum.elixirforum.com/letter_avatar_proxy/v4/letter/k/c67d28/32.png) [@krstfk](https://forum.elixirforum.com/u/krstfk)\
**Post date:** [August 27, 2020, 7:38pm UTC](https://forum.elixirforum.com/t/on-why-elixir/34038/2 "2020-08-27T19:38:18Z")

</div>

You raise some good points but

> [@shanesveller](#):
>
> I increasingly value provably correct software, which for me means an actual type system

```haskell
maximum' :: (Ord a) => [a] -> a  
maximum' [] = error "maximum of empty list"  
maximum' [x] = x  
maximum’(x:xs) = maximum’(xs)

```

In Haskell is logically wrong, and type checks. If you want probably correct software you need a theorem prover and it’s a whole new level of difficulty, that most of us can’t afford.

While true, that with some assumptions and a type system on par with the Haskell’s type system you can go a long way when refactoring ( I would highly recommend the [https://www.cs.ox.ac.uk/publications/books/functional/](https://www.cs.ox.ac.uk/publications/books/functional/)  
book to get an idea of what it’s about), it’s not a way to prove your software is correct.

We also have some pretty great tools to insure correctness : dialyzer + prop check + unit tests can go a long way.

Not to say that you’re wrong to want a strong/static type system. I wish I had it when working with elixir or erlang, but then again, the benefits of the os\_like ecosystem and the simplicity of these languages compensate the lack of static typing for me.

---

_[View the full topic](https://forum.elixirforum.com/t/on-why-elixir/34038)._