On: ZZ is a modern formally provable dialect of C

[iainmerrick]

One question that isn’t obvious from the overview:

This language compiles to C and asserts that your program will never exhibit undefined behavior; have they proved that ZZ is correct, ie that it will definitely never output C code that exhibits undefined behavior?

If you really care about correctness, that seems important. I absolutely love the idea in general though.

[pickdenis → iainmerrick]

This seems similar to bootstrapping theorem provers. Here is a HN discussion on one: https://news.ycombinator.com/item?id=21358674

[colonwqbang → iainmerrick]

It's always concerning to see a compiler not being written in the compiled language.