CakeML / CakeML/cakeml

Add example of cost proof

Open
#1,103 0 comments 0 reactions 0 assignees View on GitHub
Dominant language
Standard ML
Stars
1.2k
Forks
104
Avg merge
2d 21h
Merged PRs (30d)
16

Description

PR #1092 is aiming to remove `examples/cost` as they are currently broken. According to @myreen on Discord, the cost proofs are brittle since they work on the compiler-generated dataLang code, meaning that whenever the compiler changes, those proofs will need to be updated.

Thus, this issue tracks choosing one proof and committing to maintaining it.

Contributor guide

No contributing guide indexed for this repository

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.