karamel
KaRaMeL is a tool for extracting low-level F* programs to readable C code (by FStarLang)
cogent
Cogent Project (by au-ts)
karamel | cogent | |
---|---|---|
1 | 4 | |
384 | 157 | |
1.6% | 0.0% | |
9.3 | 0.0 | |
8 days ago | about 1 year ago | |
OCaml | Isabelle | |
Apache License 2.0 | GNU General Public License v3.0 or later |
The number of mentions indicates the total number of mentions that we've tracked plus the number of user suggested alternatives.
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.
karamel
Posts with mentions or reviews of karamel.
We have used some of these posts to build our list of alternatives
and similar projects. The last one was on 2022-11-15.
-
Let's collect relatively new research programming languages in this thread
Jasmin and F* don't have similar goals, Jasmin is a language designed to precisely express low-level code, while F* is a generalist language for verified programming. There is a subsystem of F* that performs extraction to "readable C code", Karamel (used to be called Kremlin), but you get the usual limitations of C code as a high-level assembler, and also an embedded assembly layer built on Vale. Project Everest therefore generates artifacts that are a mix of C and assembly, rather than a new low-level language design as Jasmin.
cogent
Posts with mentions or reviews of cogent.
We have used some of these posts to build our list of alternatives
and similar projects. The last one was on 2022-11-15.
-
Let's collect relatively new research programming languages in this thread
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.
-
Thoughts on the Rascal meta-programming language
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.
-
Are there any ML style languages with no runtime?
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.
-
I'm a freelancer and I've got a customer who is asking for USB driver for a new device. They want it written in c++ and I said I'd only consider creating and supporting it if it was written in Rust. 🤷♂️
https://github.com/NICTA/cogent is for auto generating isabelle theorems + C code.
What are some alternatives?
When comparing karamel and cogent you can also consider the following projects:
koika - A core language for rule-based hardware design 🦑
py4j - Py4J enables Python programs to dynamically access arbitrary Java objects
jasmin - Language for high-assurance and high-speed cryptography
edsl - Example of embedding TypeScript as an EDSL inside of another language
cubicaltt - Experimental implementation of Cubical Type Theory
programming-language-subreddits-and-their-choice-of-words - How do the different communities talk?
datafun - Research on integrating datalog & lambda calculus via monotonicity types
futhark - :boom::computer::boom: A data-parallel functional programming language
ponyc - Pony is an open-source, actor-model, capabilities-secure, high performance programming language