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
20082026
-
…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 -
…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 -
…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 -
▲ 2
ZetZ: A zymbolic verifier and tranzpiler to bare metal C Resourcesstory by tosh · 2021-05-03 · 0 comments
-
…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 -
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 -
…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 -
…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 -
…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++? -
…(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 -
…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 -
…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 -
…[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 -
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 -
…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 -
…[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) -
…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 -
…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 -
…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 -
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 -
▲ 266
ZZ is a modern formally provable dialect of Cstory by the_duke · 2020-02-05 · 153 comments