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

Not yet. Technically, this is not the first priority because effects make it drastically harder to use SMT solvers, and Cure is supposed to be used to implement critical parts of the logic and then call it from other BEAM langs.

My bad. I posted an announce too early because after a months deeply in, I was under the wrong impression that everything is evident and clean

That’s definitely not the killer feature. Despite I have put some effort to optimization, Cure does not aim to be faster. It aims to be proved to be error-free.

Disclaimer. I got a COVID and I am off the grid until next week or so. Thanks everyone for understanding. I see there is an interest in what I am doing and therefore I’ll start with a proper timeline, and feature plan. Until now I was in a rush to make it work from Cure code through type checker, code gen and runtime, which is confusing for newcomers.

I don’t think this is the case. From reading the documentation it seems that both have static type systems, but that’s where the similarities end. Gleam and Elixir have much more in common than Gleam and Cure do.

Compared to the stated features of Cure’s website Gleam offers very little in terms of static-analysis enforced correctness. If Cure’s static analysis functionality is a fighter jet then Gleam’s is a paper plane!

It will be interesting to see how the language develops. Both dependent types and SMT verification are active open areas of computer science research, and while useful and extremely powerful, how to make either of them approachable and productive in a language is an unsolved problem. Idris may be the most successful project there for dependant types, but even then it is a very challenging language to learn and write.

I couldn’t find any documentation on these features in Cure, and I wasn’t able to get any of the examples to compile and run, so I can’t say anything specific about their approach. I’m looking forward to seeing more as the language matures!

Dependant types are very slow to compile, however at runtime they can be used to produce significantly improved performance, as the compiler knows much more about the program. Unfortunately this benefit is likely not possible for Cure, as the BEAM doesn’t permit the programmer to disable runtime type checking. If it did Gleam could do that, making it substantially faster than Erlang or Elixir!

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

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.