cakeml VS Checker Framework

Compare cakeml vs Checker Framework and see what are their differences.

InfluxDB - Power Real-Time Data Analytics at Scale
Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.
www.influxdata.com
featured
SaaSHub - Software Alternatives and Reviews
SaaSHub helps you find the best software and product alternatives
www.saashub.com
featured
cakeml Checker Framework
15 12
923 991
0.9% 1.2%
9.8 9.7
3 days ago 8 days ago
Standard ML Java
GNU General Public License v3.0 or later 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.

cakeml

Posts with mentions or reviews of cakeml. We have used some of these posts to build our list of alternatives and similar projects. The last one was on 2023-10-11.
  • CakeML: A formally verified implementation of ML
    1 project | news.ycombinator.com | 14 May 2024
  • The Deep Link Equating Math Proofs and Computer Programs
    5 projects | news.ycombinator.com | 11 Oct 2023
    If I understand what you are asking about correctly, then I do think you are mistaken.

    As a sibling comment observed, you would be proving something about a program, but proving things about programs is both possible and done.

    This ranges from things like CakeML (https://cakeml.org/) and CompCert (compilers with verified correctness proofs of their optimizations) to something simple like absence of runtime type errors in statically strongly soundly-typed languages.

    Of note is that you are proving properties of your program, not proving them perfect in every way. The properties of your program that you prove can vary wildly in both difficulty and usefulness. A sufficiently advanced formally verified compiler like CakeML can transfer a high-level proof about your source code to a corresponding proof about the behavior of the generated machine-executable code.

  • The future of Clang-based tooling
    3 projects | news.ycombinator.com | 29 Jul 2023
    > A single IR with multiple passes is a good way to build a compiler

    https://mlir.llvm.org/, which is using, is largely claiming the opposite. Most passes more naturally are not "a -> a", but "a -> b". data structures and data structures work hand in hand, it is very nice to produce "evidence" for what is done in the output data structure.

    This is why https://cakeml.org/, which "can't cheat" with partial functions, has so many IRs!

    Using just a single IR was historically done for cost-control, the idea being that having many IRs was a disaster in repetitive boilerplate. MLIR seeks to solve that exact problem!

  • CakeML – A Verified Implementation of ML
    1 project | news.ycombinator.com | 5 Jun 2023
  • Tools for Verifying a Language and its Semantics
    1 project | /r/ProgrammingLanguages | 2 Jan 2023
    You may want to look at [CakeML](https://cakeml.org) done in HOL4, there is also a nice proof pearl about a more .. minimalistic verified bootstrapped compiler also in HOL4.
  • old languages compilers
    12 projects | /r/ProgrammingLanguages | 26 Dec 2022
    CakeML
  • Is there a formally-proven real-time language/computing env. or operating system?
    2 projects | /r/ProgrammingLanguages | 7 Sep 2022
    There is also Cake ML which is a formally verified functional programming language compiler and runtime.
  • CakeML: A Verified Implementation of ML
    2 projects | /r/sml | 7 Mar 2022
    There is also a CakeML -> Standard ML compiler though it seems to have been built to translate benchmarks and sort of old so I'm not sure how comprehensive it is: https://github.com/CakeML/cakeml/tree/master/unverified/front-end
  • The λ-Cube
    3 projects | news.ycombinator.com | 15 Jan 2022
    > One guess is that lisps cope with being minimal through use of macros and metaprogramming, it's difficult for a typed language to support that level of metaprogramming while maintaining the various guarantees that one wants from such a system.

    Difficult, but certainly not impossible [0].

    [0] https://cakeml.org/

  • Two Mechanisations of WebAssembly 1.0
    2 projects | /r/ProgrammingLanguages | 3 Jan 2022
    If this interests you, I'd highly recommend checking out CompCert (docs here) and CakeML.

Checker Framework

Posts with mentions or reviews of Checker Framework. We have used some of these posts to build our list of alternatives and similar projects. The last one was on 2024-04-28.
  • What if null was an Object in Java?
    3 projects | news.ycombinator.com | 28 Apr 2024
    I’m not familiar enough with kotlin to comment fully but from your description the checker framework [0] appears to do the same thing in Java.

    I confess I’m not fond of checker framework. I find the error messages can be obtuse but it is very effective.

    0 - https://checkerframework.org/

  • @Nullable et @NonNull
    1 project | dev.to | 29 Mar 2024
  • Too Dangerous for C++
    2 projects | news.ycombinator.com | 9 Feb 2024
    It is interesting! I experimented with creating a bad borrow checker for Java using annotations from

    https://checkerframework.org/

    It supports some level of substructural types using must-call annotations,

    https://checkerframework.org/manual/#resource-leak-checker

  • JEP 457: Class-File API for Parsing, generating, transforming
    2 projects | news.ycombinator.com | 26 Sep 2023
    Lombok is not a compiler extension. Compiler extensions, aka annotation processors, are offered only specific capabilities that ensure that they preserve the Java language specification. Particularly, code that compiles successfully with an extension also compiles without it (perhaps requiring other classes to be available) and it compiles down to the same bytecode. Annotation processors are used to implement pluggable type systems (e.g. https://checkerframework.org) or to generate other classes (e.g. https://immutables.github.io/).

    Unlike compiler extensions, Lombok compiles source files that do not conform to the Java language specification. Lombok is an alternative Java Platform language, like Clojure or Kotlin or Scala, except that it's a superset of the Java language. However, rather than forking `javac` source code and modifying it to compile Lombok source files, the Lombok compiler modifies `javac`'s operation by hacking into its internals and modifying them as it runs to compile Lombok sources rather than Java sources.

    Having alternative Java Platform languages is perfectly fine. The problem with Lombok is that it doesn't present itself as such but as a library or a compiler extension even though it violates the Java language specification in ways that compiler extensions are forbidden from doing.

  • I introduced Rust at work
    2 projects | /r/rust | 29 Jun 2023
    And then I found (thanks Oracle), https://checkerframework.org/ zomg, this thing is awesome. Pluggable Type Systems!
  • Checker Framework - Pluggable type systems for Java
    1 project | /r/java | 29 Jun 2023
  • Don’t call it a comeback: Why Java is still champ
    17 projects | news.ycombinator.com | 9 Aug 2022
    Java should adopt something like the Checker Framework Nullness Checker in its first-party tooling.

    https://github.com/typetools/checker-framework

  • Why Java Doesn't Support Multiple Inheritance
    1 project | /r/programming | 15 May 2022
    And modern (real, non-android) Java via project amber and so on has gone more and more quasi functional with its immutability and sealed and record types for effective sum types, as well as its pretty cool type-use annotation extensible static type checks.
  • JSpecify: Express specifications (initially, just nullness properties) in a machine-readable way
    9 projects | /r/java | 26 Jan 2022
    Checkerframework - a really academic take, and as one might expect from such a thing, backed by tons of papers and analysed to perfection. Specifically, this is the only framework I'm aware of that realizes nullity is a little more complicated than just a boolean yes-or-no; just like generics actually have 4 flavours for any given type: List, List, List, and List are all 4 important and unique, and nullity is no different. Specifically, it can occur that you want to write a method that ought to accept both lists of nullable strings as well as list of nonnull strings, and needs to 'convey' this nullity again on its output. You can either attempt to lift along the existing generics system in java which I think is your intent, but it's not actually all that easy to do this. After all, T extends @Nullable Number super @NonNull Number, or whatnot, isn't legal java. So you.. really just can't do that. Checker Framework solves this problem by introducing the @PolyNull annotation, which still isn't perfect but covers almost all real world use cases you can think of. I'm missing any acknowledgement in your documentation. An oversight, or, something you hadn't thought of yet? You're in good company: Both eclipse and intellij's engineers, when I asked them about it, just hadn't realized it was a thing. Point is: If you think the primary problem with e.g. eclipse's and intellij's take is that they lack academic rigour - checkerframework has you beat.
  • calling Format() on a time struct in a golang program changes the default Location's timezone information in the rest of the program
    4 projects | /r/programming | 3 Sep 2021
    NullAway or the Checker Framework should greatly help eliminate the issue. Also, when Java gets value types you should be able to define your own non nullable value types and use them safely.

What are some alternatives?

When comparing cakeml and Checker Framework you can also consider the following projects:

Daikon - Dynamic detection of likely invariants

hardware - Verilog development and verification project for HOL4

OpenJML - This is the primary repository for the source code of the OpenJML project. The source code is licensed under GPLv2 because it derives from OpenJDK which is so licensed. The active issues list for OpenJML development is here and the wiki contains information relevant to development. Public documentation for users is at the project website:

mpl - The MaPLe compiler for efficient and scalable parallel functional programming

CATG - a concolic testing engine for Java

CompCert - The CompCert formally-verified C compiler

JMLOK 2.0 - Tool for detecting and classifying nonconformances in Java/JML projects.

checkedc - Checked C is an extension to C that lets programmers write C code that is guaranteed by the compiler to be type-safe. The goal is to let people easily make their existing C code type-safe and eliminate entire classes of errors. Checked C does not address use-after-free errors. This repo has a wiki for Checked C, sample code, the specification, and test code.

jCUTE - Java Concolic Unit Testing Engine

smlpkg - Generic package manager for Standard ML libraries and programs

jspecify - An artifact of fully-specified annotations to power static-analysis checks, beginning with nullness analysis.

InfluxDB - Power Real-Time Data Analytics at Scale
Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.
www.influxdata.com
featured
SaaSHub - Software Alternatives and Reviews
SaaSHub helps you find the best software and product alternatives
www.saashub.com
featured