ZZ is a modern formally provable dialect of C • Hacker News Board

Re: ZZ is a modern formally provable dialect of C

#141

Post by archi42 » Wed, Feb 05, 2020, 10:16 PM UTC

whatshisface wrote: post #61

cwzwarich wrote: post #55

Earlier quoted context omitted.

> I also don't know how many cycles it takes for my implementation of quicksort apart from checking the output of a specific compiler and counting instructions. On any modern out-of-order CPU, that doesn't get you close to determining the dynamic performance. Even with full knowledge of private microarchitectural details, you'd still have a hard time due to branch prediction.

On most (small, I'm not talking about mini linux) embedded systems, instruction counting will tell you how long something takes to run. In fact, the compilers available are often so primitive that operation counting in the source code can sometimes tell you how long something will take.

Depends a lot on the compiler and target arch. You'll miss out on a lot of stack accesses, or add too many. You don't get around looking at the final executable if you want good results. And for more complex targets, in the end you need to know what the pipeline does and how the caches behave if you want a good bound on the cycle count. Of course assuming you're on anything more complex than an atmega, for which op counting might be enough. I work in the domain; lots of people do measurements, which only give a ballpark but are bad since you might miss the worst case (which is important for safety critical systems, where that latency spike in the wrong moment might be fatal). Pure op counting is bad since the results grossly overestimate (eg you always need to assume cache misses if you don't know the cache state, or pipeline stall, or DRAM, or...). Look at the complexity of PowerPC, this should give you a rough idea what we're usually dealing with (and yeah, I'm talking embedded here).

To me that "sometimes" feels like "I can wrestle some bears with my bare hands, e.g.a Teddy bear" ;-)

Re: ZZ is a modern formally provable dialect of C

#142

Post by a1369209993 » Thu, Feb 06, 2020, 12:38 AM 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.

> > program correctness

How would this language (or any other) go about verifying the correctness of:

  fn subtract(int a,int b) -> int
      model return == a + b
    {
    return a + b;
    }

Re: ZZ is a modern formally provable dialect of C

#143

Post by 0xdead » Thu, Feb 06, 2020, 1:19 AM UTC

scoutt wrote: post #5

> where we still program C out of desperation I agree it's the standard and the only thing that actually works (author's words), but it's still a pleasure for me to write and have to deal with C (for embedded). I'd be desperate if I have to be forced to deal with huge different paradigms because pointer problems or insert-your-C-rant-here . C is not going to be replaced on embedded any moment soon.

I have an anecdote to share. I work in embedded space for a living. A web developer (which is quite funny) from another team somehow convinced our director to use Rust for a critical process that involved a lot of concurrent processing. Ok, I said, and began developing that process in Rust.

I estimated that it took me about 10x the time to implement something than it would have taken if I did that in C. The reason for that could definitely be because I'm not a Rust expert at all. That's fine though because I will happily invest more time in programming if it saves me hours of debugging later. Plus, the claim that "if it compiles, it works" was enough for me to fight the compiler for hours if it gives me no trouble during runtime.

Fast forward a week, we have that binary deployed to a non-critical set of our field devices. A few days later, we get reports of that particular binary crashing. I logged into one of those devices and fetched the logs. The binary was reporting a panic on an MPSC channel's tx send. There was nothing useful in that error message that would point me to the root cause. I had no tools to attach to a running process because I'm on a device with an ancient kernel.

To fix the situtation "temporarily", because the customer is getting infuriated, we redeploy our old C binary. It has been there since. I basically now say "fuck off" to anyone who tells me to use Rust because it doesn't work if it compiles.

Re: ZZ is a modern formally provable dialect of C

#144

Post by perl4ever » Thu, Feb 06, 2020, 4:14 AM UTC

jcranmer wrote: post #76

pjmlp wrote: post #44

Earlier quoted context omitted.

We need regulation to make companies liable for CVEs, then this will stop being FUD, easy.

It says something of our profession that we have all of our products come with a legal document that effectively says it's not our fault if the product doesn't do what it's supposed to do.

We should just outlaw those damn statements (and binding arbitration for consumers) and see how the market naturally evolves. Don't force standards on programmers, don't regulate in some novel way, just get rid of the stupid disclaimers and let the old-fashioned legal framework return to primacy.

Re: ZZ is a modern formally provable dialect of C

#145

Post by yannickmoy » Thu, Feb 06, 2020, 8:21 AM UTC

pjmlp wrote: post #35

pjc50 wrote: post #22

This is a great achievement in making formal methods accessible in pragmatic terms - something that actually works and can be used by normal humans. Would be nice to have an actual microcontroller example. > The standard library is fully stack based and heap allocation is strongly discouraged :/ - I can see why this is done, as it's hard, so banning it to make the problem tractable works. But it's also quite inconven…

Unless it has changed, SPARK also forbids dynamic allocation.

It has changed: https://blog.adacore.com/pointer-based-data-structures-in-sp...

Re: ZZ is a modern formally provable dialect of C

#146

Post by twsted » Thu, Feb 06, 2020, 9:10 AM UTC

a3p wrote: post #126

loeg wrote: post #117

Earlier quoted context omitted.

What's the large project using ZZ? Or is it behind closed doors? This appears to be an entirely different ZZ programming language: https://scratch.mit.edu/discuss/topic/80752/

it is https://devguard.io/ which is being rewritten from rust to ZZ in this branch https://github.com/devguardio/carrier/tree/zz

Very interesting.

Can you tell us a little more about the reasons of the rewrite from rust?

Re: ZZ is a modern formally provable dialect of C

#147

Post by oblio » Thu, Feb 06, 2020, 10:27 AM UTC

boomlinde wrote: post #133

oblio wrote: post #38

Earlier quoted context omitted.

Well, let's say I take the Intel P54 ( https://en.wikipedia.org/wiki/List_of_Intel_microprocessors#... ) as an example. So basically an Intel Pentium from 1994, so from 26 (!) years ago. Size: 90 mm2, maximum power consumption: 10W, price at launch: $699. Buuuut: production process 600nm. Today every Intel CPU uses a 14nm production process, but let's go for a cheaper option and "use" the 22nm. So the gate size is ~3…

You are very nearly talking about the Intel Quark. They weren't very popular and Intel have since discontinued the line.

Oh, I must have missed that. They seem a bit too expensive for what I'm saying, I imagine these things have to cost cents to be worthwhile (50-70 cents or so).

Re: ZZ is a modern formally provable dialect of C

#148

Post by ksec » Thu, Feb 06, 2020, 10:52 AM UTC

oblio wrote: post #38

scoutt wrote: post #31

Earlier quoted context omitted.

The answer is size, power consumption and most of all, price. I know I can do a wrist watch with a Raspberry Pi, but will it be profitable/convenient?

Well, let's say I take the Intel P54 ( https://en.wikipedia.org/wiki/List_of_Intel_microprocessors#... ) as an example. So basically an Intel Pentium from 1994, so from 26 (!) years ago. Size: 90 mm2, maximum power consumption: 10W, price at launch: $699. Buuuut: production process 600nm. Today every Intel CPU uses a 14nm production process, but let's go for a cheaper option and "use" the 22nm. So the gate size is ~3…

Every single one of your projection is still way off compare to lowest cost embedded system. $0.3 is expensive when people are really, literally counting pennies.

Re: ZZ is a modern formally provable dialect of C

#149

Post by KarlKemp » Thu, Feb 06, 2020, 5:10 PM UTC

scoutt wrote: post #58

hurrrrrrrr wrote: post #52

Earlier quoted context omitted.

But if we get rid of a whole class of bugs and vulnerabilities, the number of bugs will go down, no?

This is a common way of thinking about it, but nobody really knows. It's purely a conjecture. There is no data to back it up, and it just appeals to common sense. Should everybody drop C/C++/whatever and rush into the Rust train because Rust people has conjecture ? I ask the opposite question. What would happen if the only programming language left is C? Wouldn't we become better programmers and raise the bar so high…

Making cars saver has dramatically reduced death and injury, and not caused the number of accident to spike. So.. no?

Re: ZZ is a modern formally provable dialect of C

#150

Post by MaxBarraclough » Thu, Feb 06, 2020, 7:32 PM UTC

a1369209993 wrote: post #142

pickdenis wrote: post #95

Earlier quoted context omitted.

> 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.

> > program correctness How would this language (or any other) go about verifying the correctness of: fn subtract(int a,int b) -> int model return == a + b { return a + b; }

This defect is obvious to anyone reviewing the code, and it will be even more obvious when the function is used by another function with its own contracts.

In practice the issue with formal modelling is that it's very hard to scale up. Modelling the correct behaviour of traffic-lights is practical, and allows us to build completely bug-free traffic-light software, but these methods don't work so well for developing a word processor. Competent practitioners don't tend to mess up their formal models though. I've not heard an example of that causing defective software, but it's a valid question to ask.

Even without going the whole way to whole-program correctness guarantees, this kind of approach can be used to provide solid guarantees against bugs like buffer-overflows, without using runtime checks. This is something the SPARK language has supported for a long time.