Zig and the design choices within • Hacker News Board

Re: Zig and the design choices within

#181

Post by smj-edison » Sat, Nov 15, 2025, 9:52 PM UTC

pron wrote: post #140

JuniperMesos wrote: post #136

Earlier quoted context omitted.

Maybe we should be using ATS. Or more likely, maybe we should be using some novel language that doesn't exist yet that brings the benefits of ATS to a language with good tooling and good DX that you can use to build practical system software with - that is, a Rust for ATS instead of C/C++. I think we should be designing programming languages that help eliminate as many classes of bug as possible, and Rust is not the…

One of the lessons of the past 50 years in software correctness is that sound guarantees are not always the most effective path to correctness. The problem is that proving something correct takes a lot of effort (and there are fundamental computational complexity reasons for that), while unsound methods are significantly cheaper and surprisingly effective in practice. A famous 1996 paper by Tony Hoare [1] expresses a…

Bit of a tangent, but what is your perspective on formal verification in hard realtime systems? Is the cost justified because the system tends to be simpler and doesn't need to evolve through time, or some other reason? Or do you see formal verification with hard realtime systems as unnecessary effort?

Re: Zig and the design choices within

#182

Post by baranul » Sun, Nov 16, 2025, 12:51 AM UTC

fransje26 wrote: post #55

guywithahat wrote: post #33

Earlier quoted context omitted.

It's interesting how much Rust has slowed down. There is still some development in linux otherwise people seem to be over it. I think Rust just doesn't offer enough in terms of features, and is overshadowed by languages like Go or C++ in terms of what developers are really looking for. Rust's popularity seems to be dropping or holding steady in indexes like TIOBE, and a lot of big "influencers" seem to be over Rust's…

> Rust's popularity seems to be dropping or holding steady in indexes like TIOBE Oh, 14th [1]. That's a lot lower than I would have expected, based purely on the amount of noise surrounding Rust. [1] https://www.tiobe.com/tiobe-index/

Think it's a matter of if a person is limiting themselves to an evangelistic echo chamber. If one confined themselves to only HN, likely to get the impression from the enthusiastic fans of Rust and Zig, that they ranked #1 and #2, where in the real world that's definitely not the case. Languages like C# (#5) and Golang (#11), rank way above Rust in the real world, but get way less shine than would be expected. It's like being a heretic, for even mentioning Object Pascal (#8), Ada (#17), or Kotlin (#20) around here. Yet, all those rank above Zig (#49). Hell, Vlang (#41) is ranked above Zig on TIOBE (November 2025).

Re: Zig and the design choices within

#183

Post by pron » Sun, Nov 16, 2025, 12:59 AM UTC

smj-edison wrote: post #181

pron wrote: post #140

Earlier quoted context omitted.

One of the lessons of the past 50 years in software correctness is that sound guarantees are not always the most effective path to correctness. The problem is that proving something correct takes a lot of effort (and there are fundamental computational complexity reasons for that), while unsound methods are significantly cheaper and surprisingly effective in practice. A famous 1996 paper by Tony Hoare [1] expresses a…

Bit of a tangent, but what is your perspective on formal verification in hard realtime systems? Is the cost justified because the system tends to be simpler and doesn't need to evolve through time, or some other reason? Or do you see formal verification with hard realtime systems as unnecessary effort?

I think formal verification can and should be used everywhere it is helpful, which certainly includes hard realtime systems but isn't limited to them (it's helpful in quite a few areas). But formal verification is by no means the same as deductive theorem proving. Especially for hard realtime systems, which tend to be simple as you say, model-checking has been the formal method of choice for decades.

Even for large, non-critical software, there are useful formal verification methods that aren't end-to-end, i.e. they can cover the design but not the code, and have proven very useful in finding bugs. I for one, am a big fan of TLA+. TLA+ has both an interactive theorem prover and a model checker (or a couple). Most importantly, it allows describing the system at an arbitrary level of detail, which means you can use it at different levels as appropriate. For some things, it can and should, say, describe hardware in full detail; for others, it can be used to describe and verify a very abstract algorithm, well above the code level.

The problem with deductive theorem proving is that it tends to have a low ROI, and there are often more effective methods. It should be used when other methods don't work well.