3 ms·

I think you are wrong in a funny way. Memory safety and memory leaks and stuff dont always matter. This sparked and interesting memory for me. I was once worki

I think you are wrong in a funny way. Memory safety and memory leaks and stuff dont always matter. This sparked and interesting memory for me. I was once working with a customer who was producing on-board software for a missile. In my analysis of the code, I pointed out that they had a number of problems with storage leaks. Imagine my surprise when the customers chief software engineer said "Of course it leaks". He went on to point out that they had calculated the amount of memory the application would leak in the total possible flight time for the missile and then doubled that number. They added this much additional memory to the hardware to "support" the leaks. Since the missile will explode when it hits it's target or at the end of it's flight, the ultimate in garbage collection is performed without programmer intervention. https://groups.google.com/g/comp.lang.ada/c/E9bNCvDQ12k/m/1tezW24ZxdAJ https://groups.google.com/g/comp.lang.ada/c/E9bNCvDQ12k/m/1t... while a funny example, you are very wrong. High assurance systems have a specification and a bazillion tests because memory safety is an insanely tiny problem in the sea of problems they face. [that is why, frama-C and friends are preferred over Rust,Ada, ATS, and whatever else that exists.] Correctness of the spec and perfectly following the spec is far more important. Zig allows correct code to feel easier to write when compared to C. Thats why it was chosen in tigerbeetle and thats why, if the community wants, it will have an insanely bright future in high assurance systems.

KsassPeuk 2y ago
As a Frama-C developer, and more precisely the deductive verification tool, I'd say that formal proof of programs (especially proof that the program conforms to its specification) would be significantly easier on Rust. The main reason is related to the handling of memory aliases which is a nightmare in C, and that generates formulas that kill SMT solvers. The consequence is that the ongoing development tend to target something that has a lot in common with Rust: we try to assume memory separation most of the time, and check that it is true on function call, but it as harder to do it than with a type system.
- samatman 2y ago
  > the handling of memory aliases which is a nightmare in C Zig has some aliasing issues which are to-date unsolved. The core and community are keenly aware of them, and they'll be solved or greatly ameliorated before a 1.0 release. It's why TigerBeetle has a coding standard which requires all container types to be passed by constant pointer, not reference. It isn't ideal, but I think it's reasonable to withhold judgement on a pre-1.0 language for some sorts of known issues which are as yet unaddressed. It's worth taking the time to find an excellent solution to the problem, rather than brute-force it or regress one of the several features which combine into the danger zone here. If you're curious or interested in the details, look up "Attack of the Killer Features" on YouTube. Given your background, I'm sure the community would value your feedback on the various issues tracking this.

KsassPeuk 2y ago

As a Frama-C developer, and more precisely the deductive verification tool, I'd say that formal proof of programs (especially proof that the program conforms to its specification) would be significantly easier on Rust. The main reason is related to the handling of memory aliases which is a nightmare in C, and that generates formulas that kill SMT solvers. The consequence is that the ongoing development tend to target something that has a lot in common with Rust: we try to assume memory separation most of the time, and check that it is true on function call, but it as harder to do it than with a type system.

samatman 2y ago
> the handling of memory aliases which is a nightmare in C Zig has some aliasing issues which are to-date unsolved. The core and community are keenly aware of them, and they'll be solved or greatly ameliorated before a 1.0 release. It's why TigerBeetle has a coding standard which requires all container types to be passed by constant pointer, not reference. It isn't ideal, but I think it's reasonable to withhold judgement on a pre-1.0 language for some sorts of known issues which are as yet unaddressed. It's worth taking the time to find an excellent solution to the problem, rather than brute-force it or regress one of the several features which combine into the danger zone here. If you're curious or interested in the details, look up "Attack of the Killer Features" on YouTube. Given your background, I'm sure the community would value your feedback on the various issues tracking this.