Hacker GitHub

← All repos

zetzit/zz

View on GitHub ↗ ★ 1,596 Rust archived

🍺🐙 ZetZ a zymbolic verifier and tranzpiler to bare metal C

21 mentions on Hacker News by 11 people: 2 stories, 19 comments · first 2020-02-05 · latest 2022-03-19

Mentions per year 21 mentions · busiest year 2020 (13)
20082026
AllStoriesComments NewestTopOldest
  1. …Sounds a lot like ZZ. [0] It also sounds much like SPARK Ada, except for transpiling to C. [0] https://github.com/zetzit/zz
    comment by MaxBarraclough · 2022-03-19 · in Kaitai Struct: A new way to develop parsers for binary structures
  2. …not its primary target. [1][2] There are several projects on formal analysis of C. [3][4][5][6] [0] https://github.com/zetzit/zz [1] https://github.com/dafny-lang/dafny [2] https://dafny-lang.github.io/dafny/ [3] https://frama-c.com/ [4]…
    comment by MaxBarraclough · 2022-01-23 · in ISO C became unusable for operating systems development
  3. …aim to make formal software development much easier [0][1] and of course there's SPARK Ada. [0] https://github.com/zetzit/zz [1] https://github.com/dafny-lang/dafny
    comment by MaxBarraclough · 2021-11-21 · in Foundations of Dawn: The Untyped Concatenative Calculus
  4. …programming language, and seems to do a lot of what the post talks about automatically. [0] https://github.com/zetzit/zz
    comment by sweetsocks21 · 2021-05-03 · in Programming in Z3 by learning to think like a compiler
  5. I still want to try the ZZ language ( https://github.com/zetzit/zz ) someday. It compiles to C, and uses a SMT solver to prove that you don't index out-of-bounds at compile time. But I don't like how it lacks generics, uses C idioms, and…
    comment by nyanpasu64 · 2021-04-03 · in Grids in Rust, Part 2: const generics
  6. …high hopes for the zz language. Especially the fact that it outputs C code. So interop is seamless. https://github.com/zetzit/zz For any systems language, interop with C is the litmus test. With that in mind, this new language should not…
    comment by jpfr · 2021-03-19 · in We are building a new systems programming language
  7. …Nim, and perhaps Vala. Also the lesser-known ZZ and Dafny languages, which look very interesting. https://github.com/aep/zz https://github.com/dafny-lang/dafny
    comment by MaxBarraclough · 2021-02-17 · in Inline and Sideline Approaches for Low-Cost Memory Safety in C
  8. …to mandate the absence of serious compiler optimisations, especially for a language like C. [0] https://github.com/zetzit/zz [1] https://github.com/microsoft/Armada
    comment by MaxBarraclough · 2020-09-24 · in How expensive is integer-overflow trapping in C++?
  9. …(I figure you know this already, pjmlp, but it might be useful for someone else) [1] https://github.com/aep/zz , see also https://news.ycombinator.com/item?id=22245409
    comment by MaxBarraclough · 2020-09-14 · in Nvidia's Arm deal sparks quick backlash in chip industry
  10. …they're not 'quick fix' solutions, so they're not widely used. https://www.eschertech.com/products/ https://github.com/zetzit/zz https://blog.regehr.org/archives/1069 (ctrl-f for actually )
    comment by MaxBarraclough · 2020-09-02 · in Tips for stable and portable software
  11. …C Verifier, [4] both of which work with C directly. [0] https://jamesrwilcox.com/armada.pdf [1] https://github.com/zetzit/zz [2] https://news.ycombinator.com/item?id=22245409 [3] http://frama-c.com/acsl_tutorial_index.html [4]…
    comment by MaxBarraclough · 2020-07-30 · in Dafny: Verification-Aware Programming Language
  12. …[1] https://en.wikipedia.org/wiki/SPARK_(programming_language) [2] https://github.com/aep/zz [3] https://news.ycombinator.com/item?id=22245409 [4] https://www.eschertech.com/articles/index.php
    comment by MaxBarraclough · 2020-04-07 · in The SeL4 Foundation: What and Why
  13. Link to ZZ itself is way down the article. Here it is for convenience: https://github.com/aep/zz
    comment by NonEUCitizen · 2020-03-31 · in So long rust, why I built ZZ
  14. …keep using the language because of the ABI. Rather ZetZ -- Symbolic Verifier and Transpiler to C. https://github.com/aep/zz and previous discussions, https://news.ycombinator.com/item?id=22245409 Zig, https://ziglang.org/…
    comment by sitkack · 2020-03-29 · in Effective C: An Introduction to Professional C Programming
  15. …[2]. But perhaps I'm digressing. [0] https://en.wikipedia.org/wiki/SPARK_(programming_language) [1] https://github.com/aep/zz [2] https://news.ycombinator.com/item?id=22245409
    comment by MaxBarraclough · 2020-03-20 · in Exploring calling conventions with x86 assembly (2016)
  16. …heap-free targets (microcontrollers) such as tail variants (statically enforced flexible arrays): https://github.com/aep/zz#metaprogramming-or-templates-tail-...
    comment by a3p · 2020-02-05 · in ZZ is a modern formally provable dialect of C
  17. …there's a example of proving a simple state machine open > read > close [1] Just read the docs™ [1] https://github.com/aep/zz#theory
    comment by augusto-moura · 2020-02-05 · in ZZ is a modern formally provable dialect of C
  18. …thread, their project summary isn't clear about this. Still a great idea for a language though. [0] https://github.com/aep/zz/tree/master/examples/hello/src
    comment by MaxBarraclough · 2020-02-05 · in ZZ is a modern formally provable dialect of C
  19. I think I found some FFI examples: - Using ZZ struct in C: https://github.com/aep/zz/tree/master/tests/mustpass/inlinei... - Using C code in ZZ: https://github.com/aep/zz/tree/master/tests/mustpass/ctype_i...
    comment by speps · 2020-02-05 · in ZZ is a modern formally provable dialect of C