4 ms·

> You need to add explicit bounds check or explicitly allocate in C though. It is not there if you do not add it yourself. Yes — in C you can skip the bounds-c

> You need to add explicit bounds check or explicitly allocate in C though. It is not there if you do not add it yourself. Yes — in C you can skip the bounds-checks and allocation, because you can convince yourself they aren't needed; the problem is you may be wrong, either immediately or after later refactoring. In other memory-safe languages you don't risk the buffer overrun, but it's likely you'll get the bounds checks and allocation, and you have the overhead of GC. Rust is close to alone in doing both.

johnisgood 2y ago
Rust is not the only one, there is Ada as well. Ada without SPARK adds bounds checks (which can be disabled through a compiler option), but with SPARK, it does not have to be done at runtime, among many other things (contract-based programming (without SPARK), formal verification (with SPARK) where you need it, and so forth), everything as a breeze. https://docs.adacore.com/spark2014-docs/html/ug/en/usage_scenarios.html https://docs.adacore.com/spark2014-docs/html/ug/en/usage_sce... Look at the table after this paragraph: > 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. This is the documentation (namely SPARK User's Guide). As for what SPARK is: https://learn.adacore.com/courses/intro-to-spark/chapters/01_Overview.html#what-is-it https://learn.adacore.com/courses/intro-to-spark/chapters/01..., so you will be able to see (if you read further), that Ada alone may suffice for the majority of the cases, as for many things you do not even need SPARK to begin with. Many courses for both Ada and SPARK are available here: https://learn.adacore.com/index.html https://learn.adacore.com/index.html There are very good reasons for why Ada is used in critical systems, especially, but not limited to avionics and railway systems, see more at https://www.adacore.com/industries https://www.adacore.com/industries.

johnisgood 2y ago

Rust is not the only one, there is Ada as well. Ada without SPARK adds bounds checks (which can be disabled through a compiler option), but with SPARK, it does not have to be done at runtime, among many other things (contract-based programming (without SPARK), formal verification (with SPARK) where you need it, and so forth), everything as a breeze. https://docs.adacore.com/spark2014-docs/html/ug/en/usage_scenarios.html https://docs.adacore.com/spark2014-docs/html/ug/en/usage_sce... Look at the table after this paragraph: > 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. This is the documentation (namely SPARK User's Guide). As for what SPARK is: https://learn.adacore.com/courses/intro-to-spark/chapters/01_Overview.html#what-is-it https://learn.adacore.com/courses/intro-to-spark/chapters/01..., so you will be able to see (if you read further), that Ada alone may suffice for the majority of the cases, as for many things you do not even need SPARK to begin with. Many courses for both Ada and SPARK are available here: https://learn.adacore.com/index.html https://learn.adacore.com/index.html There are very good reasons for why Ada is used in critical systems, especially, but not limited to avionics and railway systems, see more at https://www.adacore.com/industries https://www.adacore.com/industries.