ZZ is a modern formally provable dialect of C

Post by throwaway17_17 » Wed, Feb 05, 2020, 5:10 PM UTC

marta_morena wrote: post #87

This is just another symptom of why OpenSource often sucks. Instead of somehow coordinating and focusing their efforts, everyone seems to need to start their own spin off "inspired" by other projects. When do people realize that building a new language is almost always going to fail and only very very few languages ever reach anything close to adoption. Instead of spending all this time writing your own doomed langua…

Post by Jaxan » Wed, Feb 05, 2020, 5:14 PM UTC

fuklief wrote: post #16

Jaxan wrote: post #7

I like how they incorporate an SMT solver. They claim: “all code is proven”. What does that mean? What is proven about the code? Absence of memory bugs, or actual correctness of algorithms?

+1 What does it even mean that the language is formally provable ?!

Post by pickdenis » Wed, Feb 05, 2020, 5:38 PM UTC

MaxBarraclough wrote: post #79

I find the basic idea of this project to be very compelling - I was thinking aloud on HN recently and arrived at roughly the idea this project is implementing. [0] With that said, I really dislike the way they're describing their project. When I read safe dialect of C , I first assumed they meant they had developed a safe subset of C, or perhaps a very similar language, like OpenCL C [1]. Instead, they developed a ne…

  fn bla(int a) -> int
      model return == 2 * a
  {
      return a * a;
  }

Post by MaxBarraclough » Wed, Feb 05, 2020, 5:43 PM UTC

pickdenis wrote: post #95

MaxBarraclough wrote: post #79

I find the basic idea of this project to be very compelling - I was thinking aloud on HN recently and arrived at roughly the idea this project is implementing. [0] With that said, I really dislike the way they're describing their project. When I read safe dialect of C , I first assumed they meant they had developed a safe subset of C, or perhaps a very similar language, like OpenCL C [1]. Instead, they developed a ne…

> Your language does not allow me to prove program correctness Isn't that the whole point of the SMT solver? What about this example (that doesn't compile)? fn bla(int a) -> int model return == 2 * a { return a * a; } Isn't that verifying program correctness? A sibling of this comment claims that "the only thing proven is memory access validity" but, again, this example takes that down.

Post by Accujack » Wed, Feb 05, 2020, 6:00 PM UTC

AstralStorm wrote: post #77

Accujack wrote: post #74

Earlier quoted context omitted.

Or anywhere else. Lots of people don't enjoy using C for various reasons, but generally programmers don't get to choose what language they work in, they get paid to work in whatever language is needed. Whether programmers like it or not for non personal projects doesn't actually matter too much. If you don't like using C, then don't take jobs programming in C. Just don't whine when that makes it more difficult to get…

It does matter if the reasons why they do not like it are good. Decision makers should listen to such input instead of deciding on programming language by fiat or convention. Including hardware choices. Of course this should be weighted by market availability and cost of both hardware and programmers. Typically the reason C is used because there's no other toolchain available for said embedded device, except assemble…