effekt VS cogent

I like it. Modern languages that distinguish between pure and impure programs like Flix, Koka, and Effekt do so on the type level instead of syntactically. This has three advantages:

The problem with checked exceptions been identified and solved. The same problem and solution applies to effect handlers. Effekt is a language with lexical effect handlers which doesn't have this problem. Consider the following program in Effekt:

Yes, for you this is the right decision. But for us going to CPS makes everything significantly easier and in cases where you do use control effects significantly faster. For our language Effekt we are exploring different tradeoffs in different backends.

This pattern they observe is nicely captured by effect handlers. These examples are written in Effekt.

This is beyond my level of expertise. But effect tracking? There are some cool languages out there that do that consistently! Search for "algebraic effects". My favorite is Koka. Effekt also seems to be a popular choice.

https://effekt-lang.org/ A research language with effect handlers and lightweight effect polymorphism

Examples are languages like Koka, Effekt, Links, or Unison. These languages come with a type-and-effect system: a function's type not only tell you which values the function accepts and which values it returns, but also which effects it has. This is relevant to your question, because throwing an exception is one such effect.

It seems that with Effekt we are pursuing the same goal, but coming from the opposite direction, perhaps one day we will meet in the middle :). We start from a purely functional language and carefully add effects like mutation.

- https://effekt-lang.org/

Cogent, late 2010s, a language with linear types for verification. The idea is that you write functional-looking code that is easy to verify using the functional semantics, but with an efficient compilation strategy enabled by linear types to get realistic system programs.

Of course. Here was the first incarnation: https://github.com/amw-zero/sligh. It has a decent overview of the idea in the readme. To sum it up here, the idea is: have a language built around model-driven development and model-based testing, where you write a simple model of an application, and the implementation and model-based tests are compiled for you. I wrote about the overall model-based testing strategy here. This idea comes from self-certifying compilers that produce proofs of their correctness such as Cogent, but we drop the formality requirement and use property-based testing to compare the implementation and model.

That made me think of this project Cogent. This is almost certainly not what you’re looking for, because it’s aimed at formal verification. But, it does have some interesting properties, like manual memory management through uniqueness types. It doesn’t even support recursion though so, probably not so good as a general purpose PL.

https://github.com/NICTA/cogent is for auto generating isabelle theorems + C code.