Hacker GitHub

← All repos

CakeML/cakeml

View on GitHub ↗ ★ 1,225 Standard ML

CakeML: A Verified Implementation of ML

12 mentions on Hacker News by 12 people: 2 stories, 10 comments · first 2015-03-02 · latest 2025-11-21

Mentions per year 12 mentions · busiest year 2019 (3)
20082026
AllStoriesComments NewestTopOldest
  1. I have not heard of Pancake, seems interesting. It led me to https://cakeml.org . Looking at https://github.com/CakeML/cakeml/blob/3194e00b69ce817cf47751... , I feel quite dumb. :P
    comment by johnisgood · 2025-11-21 · in The Lions Operating System
  2. …EDIT: also this: https://github.com/rationalis/pancake Ah, its in here: https://github.com/CakeML/cakeml/
    comment by lamontcg · 2023-10-04 · in Pancake: Verified Systems Programming Made Sweeter [pdf]
  3. …is ongoing to reuse much of the compiler infrastructure for 'pancake', a low-level language. 0. https://github.com/CakeML/cakeml
    comment by moonchild · 2021-06-27 · in CompCert – Formally-verified C compiler
  4. …no one can have a conversation with you. [0] https://www.idris-lang.org/idris-1-1-1-released/ [1] https://github.com/CakeML/cakeml/issues/438 [2] https://stackoverflow.com/questions/56227629/segmentation-fa... [3]…
    comment by shakna · 2019-12-19 · in Make CPython segfault in 5 lines of code
  5. https://github.com/CakeML/cakeml/issues/111
    comment by xrchz · 2019-01-06 · in The Verified CakeML Compiler Back End [pdf]
  6. The example implementation of Unix cat(1) is... intimidating! https://github.com/CakeML/cakeml/blob/master/examples/iocatP...
    comment by frou_dh · 2018-11-21 · in CakeML – A Verified Implementation of ML
  7. …designed compiler and language. ;) EDIT to add: Ocaml syntax is being worked on at link below. https://github.com/CakeML/cakeml/tree/master/unverified/ocam...
    comment by nickpsecurity · 2017-01-01 · in CakeML – A Verified Implementation of ML
  8. It seems that there are some examples here: https://github.com/CakeML/cakeml/blob/master/explorer/exampl... Whould be cool to have these examples accessible from the web interface of the compiler explorer.
    comment by clarus · 2017-01-01 · in CakeML – A Verified Implementation of ML
  9. …(S)ML extensions have formal semantics as well, and OCaml itself is partially specified [2]. [1] https://github.com/CakeML/cakeml [2] http://www.cl.cam.ac.uk/~so294/ocaml
    comment by jallmann · 2015-05-21 · in OCaml 4.03 will, “if all goes well”, support multicore
  10. …https://cakeml.org/ Not that this project, unlike CompCert, is Free Software in the Stallman sense: https://github.com/CakeML/cakeml/blob/master/COPYING
    comment by jbapple · 2015-03-02 · in CompCert: A formally verified optimizing C compiler