Cure - a new language compiled to BEAM

Chat / Discussions
, , ,
1

I am happy to introduce the very α version of the new programming language compiled to BEAM.

Welcome Cure.

It has literally three killer-features:

  • Dependent types (think Idris) with SMT-solvers
  • FSMs with SMT-validation as a language primitive
  • No if-then-else construct.

I created Cure more as an ad-hoc DSL, rather than as a general purpose language. Currently it is in the proof of concept stage, although everyone might grab it, compile it, write and execute some code with it.

I am very open to suggestions, improvements, hints, and “this is all crap” comments.

51 Likes
2

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

3

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.

3 Likes
4

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…

1 Like
5

Congratulations @mudasobwa :tada:

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 :icon_biggrin:

8 Likes
6

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/.

2 Likes
7

Thanks!

Yeah, I eventually will.

2 Likes
8

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 :clap:

4 Likes
9

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
10

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

1 Like
11

Yeah, my bad. Will fix it. The website has a link to ex_doc generated from erlang sources though: Cure Programming Language — cure v0.1.0 which in turn has links to the repository.

1 Like
12

Actually the source_url link was broken. Here you go :smiley:

3 Likes
13

Congrats! An impressive effort.

Btw, looking at the docs..

`def next(fsm: FSM(TrafficLight)): FSM(TrafficLight) =     `
`  fsm_send(fsm, pair(:timer, unit()))`

Why FSM( TrafficLight) in the header if TrafficLight is already defined as a FSM?

Also why let for assignment? Is it for symmetry with function’s def then =? If so, then why the function’s = in the first place? record definition requires a do/end, why not stick to it elsewhere (like in Elixir :)?

IMO, the only thing more annoying than let is := (which you luckily don’t use)

14

This is a dependent type, if I correctly understood the question.

Well, in BEAM languages = means match. People get accustomed to this and they do expect 1 = x to compile (assuming x has been assigned to 1 before.) Cure does not support in-place matches (yet?).

Also, it made way simpler to experiment with in-place matches without breaking things, because x = 1 is currently would raise at compile stage (thanks let.)

THe syntax, though, is not yet 102% settled. = in function declarations might have changed later too. Parser is isolated and might be easily modified.

2 Likes
15

Thanks, merged. The website must be extensively improved, of course.

1 Like
16

Looks amazing! The examples link on the website returns 404. https://cure-lang.org/examples/

Where can I see some examples?

2 Likes
17

I promise I’ll fix the site sooner or later :slight_smile:

Also, the standard library is all written in Cure itself cure-lang/lib at main · am-kantox/cure-lang · GitHub

2 Likes
18

I like the idea of seeing Dependent Types getting more adoption. I think they’re a feature that should be adopted into more languages.

2 Likes
19

Easier to say than to implement :slight_smile:

The issue is probably almost nobody actually wants to sacrifice the development speed to get a proof of code correctness, like the one SMT-solver provides. In 99% of cases just let it crash works.

2 Likes
20

This may be true but I’m excited about the prospect of being able to e.g. safely code a medical device on the BEAM.

My big question would be what problems does this solve that Gleam doesn’t?

Gleam also uses strict GADTs and exhaustive pattern matching. In theory if it compiles, then correctness has been proved.

But I don’t know enough about dependent types to know how they differ. Also I love the idea of FSMs being a first class citizen.

1 Like