Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

An intro to Zig's integer casting for C programmers

lagerdata.com

Post reply on HN
Print view View original

51–60 of 135 posts

Re: An intro to Zig's integer casting for C programmers

#51

Post by johnisgood »

steveklabnik wrote: post #19
johnisgood wrote: post #8

Earlier quoted context omitted.

Yeah, and Ada/SPARK performs those checks people are hyped about (and more) at compile-time! Honestly, Ada does everything those languages do (regarding safety), and does more and does it better (again, talking about safety and correctness here). If you want evidence, check out my posts: https://news.ycombinator.com/item?id=19122884 (!) https://news.ycombinator.com/item?id=19245898 (!!) https://news.ycombinator.com/i…

Most of Rust's checks are at compiletime, and Ada employs runtime checks as well.

It can employ, but you do not have to (you can turn off all runtime checks and use formal verification only, something that Rust cannot do (statically verify correctness the same way you can with SPARK using GNATprove)), it can all be done at compile-time with Ada/SPARK.

> These runtime checks[1] are costly, both in terms of program size and execution time. It may be appropriate to remove them if we can statically ensure they aren't needed at runtime, in other words if we can prove that the condition tested for can never occur.

> This is where the analysis done by GNATprove comes in. It can be used to demonstrate statically that none of these errors can ever occur at runtime. Specifically, GNATprove logically interprets the meaning of every instruction in the program. Using this interpretation, GNATprove generates a logical formula called a verification condition for each check that would otherwise be required by the Ada (and hence SPARK) language.

Additionally, in Ada/SPARK, you can formally verify tasks (concurrency), too: https://docs.adacore.com/spark2014-docs/html/ug/en/source/co....

Moreover:

> SPARK builds on the strengths of Ada to provide even more guarantees statically rather than dynamically. As summarized in the following table, Ada provides strict syntax and strong typing at compile time plus dynamic checking of run-time errors and program contracts. SPARK allows such checking to be performed statically. In addition, it enforces the use of a safer language subset and detects data flow errors statically.

Contract programming:

- Ada: dynamic

- SPARK: dynamic / static

Run-time errors:

- Ada: dynamic

- SPARK: dynamic / static

Data flow errors:

- Ada: -

- SPARK: static

Strong typing:

- Ada: static

- SPARK: static

Safer language subset:

- Ada: -

- SPARK: static

Strict clear syntax:

- Ada: static

- SPARK: static

Additionally, safe pointers in SPARK: https://blog.adacore.com/using-pointers-in-spark and https://arxiv.org/abs/1710.07047.

More information about Get_Line (i.e. even where you would think you cannot go static): https://blog.adacore.com/formal-verification-of-legacy-code.

[1] overflow check, index check, range check, divide by zero

Re: An intro to Zig's integer casting for C programmers

#52

Post by kaba0 »

TchoBeer wrote: post #44
AnIdiotOnTheNet wrote: post #6

Earlier quoted context omitted.

> Make something idiot-proof and the world invents a better idiot. Sure, but if you only ever give people safety scissors then you're severely limiting the kinds of things that they can build. You have to let people who know what they are doing be able to do what they need to do, so you have to be able to turn the runtime safety off. Zig can do this at the scope level.

I don't understand why there aren't any solutions like this. Why aren't there any languages with a good garbage collector but also let you turn it off and work with memory manually. Maybe there is and I don't know of it? Maybe garbage collected languages and manual memory languages require different design? I don't know.

Well, GC languages can’t really allow arbitrary pointer arithmetic (because it would make GC useless/unsafe), but languages that can do explicit stack—allocation are numerous, like C#, Go, I’m sure D as well. Nim also has an optional GC, so there are languages all around the spectrum.

Re: An intro to Zig's integer casting for C programmers

#53

Post by johnisgood »

gilnaa wrote: post #10
lionkor wrote: post #2

> If runtime safety is turned off, you get undefined behavior You already know someone will teach their students to always have it off because its "slower" or something. Make something idiot-proof and the world invents a better idiot. Another language that does safety like this incredibly well is Ada (Ada/SPARK), and I'm unsure why people aren't more hyped about it. So many people hype Rust or Zig or whatever new lan…

Not to sound too aggressive, I'm not sure why ada programmers keep being surprised at the hype. Safety (of all kinds) is not the only selling point of Rust and Zig, and the fact that Ada also have safety measures doesn't mean that it's instantly an option for me. For example, I keep seeing people hype about Zig/Rust, for all kinds of reasons; and the way that they present their arguments is very compelling. While I'v…

> I don't like Rust because it gives me memory safety, tons of languages do that. I love Rust because the tradeoffs it gives me worth the switch, and the overall tooling and ecosystem are very well made.

Same applies to the tooling of Ada/SPARK, but as you have said, it is pretty much a PR issue.

Re: An intro to Zig's integer casting for C programmers

#54

Post by steveklabnik »

bbatha wrote: post #39
pornel wrote: post #29

Earlier quoted context omitted.

Rust does go overboard though, e.g. indexing requires `usize`. You either use `usize` for all your integers, or you end up with a cast-salad. arr[i as usize] This is actually risky, because even when you only meant to extend, you can also accidentally truncate or change sign. `as` does all of these things without a warning, and mixed with type inference it can easily lead to surprises. Rust makes it worse by insistin…

As I'm sure you're aware, this gets lost in bike shed land every time it comes up but Rust could implement `Index ` pretty easily. Unlike C you don't need an implicit cast to do the right thing. Personally, I have datastructure that uses non `usize` indexes I usually wrap my vector/array in in a custom type that implements index on whatever my common index types are.

It's not only "bikeshedding", there are (in my understanding) significant inference issues that happen if we were to enable this, and that would have to be dealt with in a satisfactory way.

Re: An intro to Zig's integer casting for C programmers

#55

Post by johnisgood »

StreamBright wrote: post #33
lionkor wrote: post #2

> If runtime safety is turned off, you get undefined behavior You already know someone will teach their students to always have it off because its "slower" or something. Make something idiot-proof and the world invents a better idiot. Another language that does safety like this incredibly well is Ada (Ada/SPARK), and I'm unsure why people aren't more hyped about it. So many people hype Rust or Zig or whatever new lan…

> Make something idiot-proof and the world invents a better idiot. :D My argument is that if I need that insane speed and safety features have to be off I should actively work for that not the other way around that I should actively work for safety. Why? Because we forget to do things. > Another language that does safety like this incredibly well is Ada (Ada/SPARK) I wanted to learn Ada for a long time. Do you have a…

I once collected all of my posts about Ada which do contain lots of links that can get you started. I will not re-post them here, instead you may go to https://news.ycombinator.com/item?id=23808305. Check out the links under [2].

Especially these ones: https://news.ycombinator.com/item?id=21435869 and https://news.ycombinator.com/item?id=21437498

Re: An intro to Zig's integer casting for C programmers

#56

Post by dnautics »

gilnaa wrote: post #10
lionkor wrote: post #2

> If runtime safety is turned off, you get undefined behavior You already know someone will teach their students to always have it off because its "slower" or something. Make something idiot-proof and the world invents a better idiot. Another language that does safety like this incredibly well is Ada (Ada/SPARK), and I'm unsure why people aren't more hyped about it. So many people hype Rust or Zig or whatever new lan…

Not to sound too aggressive, I'm not sure why ada programmers keep being surprised at the hype. Safety (of all kinds) is not the only selling point of Rust and Zig, and the fact that Ada also have safety measures doesn't mean that it's instantly an option for me. For example, I keep seeing people hype about Zig/Rust, for all kinds of reasons; and the way that they present their arguments is very compelling. While I'v…

> Sounds like a PR problem, mostly.

It's the case that the Zig creator did put a high priority on soft "PR" for the language, the first hire was a developer advocate/community manager. I think this is a great case of "lessons learned" from the history of programming languages.

Re: An intro to Zig's integer casting for C programmers

#57

Post by dnautics »

TchoBeer wrote: post #44
AnIdiotOnTheNet wrote: post #6

Earlier quoted context omitted.

> Make something idiot-proof and the world invents a better idiot. Sure, but if you only ever give people safety scissors then you're severely limiting the kinds of things that they can build. You have to let people who know what they are doing be able to do what they need to do, so you have to be able to turn the runtime safety off. Zig can do this at the scope level.

I don't understand why there aren't any solutions like this. Why aren't there any languages with a good garbage collector but also let you turn it off and work with memory manually. Maybe there is and I don't know of it? Maybe garbage collected languages and manual memory languages require different design? I don't know.

for erlang, if you drop down to C you completely lose the garbage collector, but the docs for doing this show you how to set up a hook for your memory to be garbage collected just like any other first-class data in the system.

If you're really responsible, it's possible to use the system allocator to inform the system about how much memory your allocations consume so that the memory pressure triggers have a correct accounting of how much memory is being used.

Re: An intro to Zig's integer casting for C programmers

#58

Post by scoutt »

I am curious to know the reasons behind the @as() syntax. What's wrong with "i32 y = (i32) x;"?

I look with interest to new languages but after so many years dealing with C, my parser crashes when I see the type after the variable name and at the end of functions declarations.

    var x : u8 = 5;
What's wrong with "u8 x = 5;"?

And I don't really like type inference very much (or when it's abused or cannot be avoided). What is "b"? Oh, I have to check what it's being casted from...

    var a: u8 = 255;
    var b = 1 + 2 + 3 - (4 + @as(i32, a));
What type is "b"? i32?

Curious fact: the above code generates >40000 lines of assembly in godbolt: https://www.godbolt.org/z/fxfbb9jfn

Re: An intro to Zig's integer casting for C programmers

#59

Post by StreamBright »

johnisgood wrote: post #55
StreamBright wrote: post #33

Earlier quoted context omitted.

> Make something idiot-proof and the world invents a better idiot. :D My argument is that if I need that insane speed and safety features have to be off I should actively work for that not the other way around that I should actively work for safety. Why? Because we forget to do things. > Another language that does safety like this incredibly well is Ada (Ada/SPARK) I wanted to learn Ada for a long time. Do you have a…

I once collected all of my posts about Ada which do contain lots of links that can get you started. I will not re-post them here, instead you may go to https://news.ycombinator.com/item?id=23808305 . Check out the links under [2]. Especially these ones: https://news.ycombinator.com/item?id=21435869 and https://news.ycombinator.com/item?id=21437498

Thanks!

Re: An intro to Zig's integer casting for C programmers

#60

Post by messe »

scoutt wrote: post #58

I am curious to know the reasons behind the @as() syntax. What's wrong with "i32 y = (i32) x;"? I look with interest to new languages but after so many years dealing with C, my parser crashes when I see the type after the variable name and at the end of functions declarations. var x : u8 = 5; What's wrong with "u8 x = 5;"? And I don't really like type inference very much (or when it's abused or cannot be avoided). Wh…

> Curious fact: the above code generates >40000 lines of assembly in godbolt: https://www.godbolt.org/z/fxfbb9jfn

I took a quick glance at the ASM, and it seems that the majority of that is code from the stdlib run prior to main. Compiling with -OReleaseSafe brings that down to 15,000 lines of assembly.

If you get rid of "main" and compile it as an exported function, you get far less code: https://www.godbolt.org/z/jjGP4xsfx

If you add -OReleaseSafe to the "export fn" version I shared, it's around 4 lines of code calling panic. Adding -OReleaseFast, and it's just a ret statement.

Post reply on HN