Cure - a new language compiled to BEAM

Interesting , could you elaborate on what problem arose with regular beam languages for you to create the lang/dsl? I imagine it didnt just chuck down to elixir and erlang not being statically typed, also I thought dependent types were more on the theoretical side and arent really used for applications in the industry, ive played around with idris because of the thinking in types book and did enjoy using the type as a value and vice versa

edit:

Just to clarify on what I mean by “problem”, I understand beam languages arent typed but Ive been under the assumption that beam fault tolerance/”let it crash” primitives cleans up on this area in terms of safety and correctness

They don’t. Sending the mistyped message (:ook instead of :ok) to the arbitrary process won’t bring any harm whatsoever, but the application would be obviously misfunctional; assigning a negative value to the latitude won’t bring any harm, etc.

In Cure, if FSM has been compiled, it’s proven to be correct. The compiler won’t let you send a message to it which won’t be understood and handled.

I was simply tired to implement critical parts in Idris and then transate the code to Elixir once proved to be correct.

Just as an example: in Cure, List.reverse/1 is proven to be correct implementation. No tests are ever needed. That is also true for some user-defined functions.

This is super cool and incredibly useful. It could be interesting to position this as something similar to LiquidHaskell but for BEAM.

I would love to use these features within elixir though…

Congratulations @mudasobwa

I’ve moved the thread here from libraries as it does not appear to be used within Elixir (if it is let me know and we can move it back).

Must admit I do not know much about FSMs and SMT verification myself (and I can’t be the only one) so it may be worth explaining in a bit more detail why those things are important enough to become a fundamental compelling part of your/a new language

Tehchnically, you can, because Cure compiles to BEAM. You can use these features with Elixir as you can use erlang with Elixir (:math.pi().) If you are talking about using it with Elixir syntax, or directly from Elixir as a library, or like, it’s impossible, because Cure compiles to BEAM using its own compiler, I cannot use Elixir compiler because of SMT solver and FSMs validation.

I have plans of introducing a bridge (through Elixir compiler,) so that one might have Cure code in cure/ directory like you have erlang in src/.

Thanks!

Yeah, I eventually will.

This seems very interesting! Ever since I first tried out Idris I’ve loved the idea of dependent types – and now you’re telling me I might use them on BEAM? Congrats on reaching this milestone

Standard library (which is tiny yet, I implemented only what I needed myself atm) already does:

  # Basic operations
  def length(v: Vector(T, n)): Nat = n
  def is_empty(v: Vector(T, n)): Bool = n == 0

I’ve been trying to look at the website on my phone, and I can’t see any links to downloads or a git repository? Does a public git repository exist or is it not out yet?

Edit: ah, never mind you mention it in the original post itself, but not on the website I guess

Yeah, my bad. Will fix it. The website has a link to ex_doc generated from erlang sources though: https://cure-lang.org/api/readme.html which in turn has links to the repository.