<story><title>Welcome to Comprehensive Rust</title><url>https://google.github.io/comprehensive-rust/</url></story><parent_chain><item><author>eggy</author><text>I still play with Rust (and Zig), but I have decided to put my work efforts into SPARK[1], the subset of Ada, for high-integrity software and formal verification. I know AdaCore and Ferrous Systems are collaborating in trying to bring a lot of Ada&amp;#x2F;Spark&amp;#x27;s capabilities to Rust, but this is still going to be some time. Ada has a longer legacy in this game.&lt;p&gt;I am working on safety critical control systems and there is a lot to prune from existing work in this area in SPARK and Ada.&lt;p&gt;This book[2], &amp;quot;Building High Integrity Applications with SPARK&amp;quot; really sold me on the benefits. It is a great intro of how SPARK was used for the CubeSat program at Vermont Technical College (VTC). A CubeSat was successfully launched in 2013. I could not find any critical mission software written in Rust yet especially that far back.&lt;p&gt;I found Julia&amp;#x27;s selection for a flight collision avoidance system perplexing[3], but it proves a PLs syntax and evangelism (maybe not in this case), can bias a selection of a PL for such tasks.
People find Ada&amp;#x2F;SPARK&amp;#x27;s syntax and methods verbose and similar to Pascal or other PLs, however, I was up and running quickly in it as opposed to Rust.&lt;p&gt;You can program to bare metal in SPARK, and the tools are already there to provide high-integrity software. The tools for SPARK automate most of the verification. Most of Rust&amp;#x27;s wishlist is already in SPARK (and Ada). I hope the Ferrous Systems and AdaCore collab bears fruit for Rust, but I have been programming since 1978, and I play with many PLs, but I found Rust&amp;#x27;s initial learning curve very off putting and I don&amp;#x27;t have the time to wait for it to mature to SPARK&amp;#x27;s level. And this is from someone who loves J&amp;#x2F;APL&amp;#x2F;BQN and Lisp, so I have no issue with different programming paradigms. I found Zig much easier to get things done from the start, although it does not strive to be a SPARK or Rust.&lt;p&gt;[1]  &lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;www.adacore.com&amp;#x2F;sparkpro&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;www.adacore.com&amp;#x2F;sparkpro&lt;/a&gt;&lt;p&gt;[2]  &lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;www.amazon.com&amp;#x2F;Building-High-Integrity-Applications-SPARK&amp;#x2F;dp&amp;#x2F;1107040736&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;www.amazon.com&amp;#x2F;Building-High-Integrity-Applications-...&lt;/a&gt;&lt;p&gt;[3]  &lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;juliahub.com&amp;#x2F;case-studies&amp;#x2F;lincoln-labs&amp;#x2F;&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;juliahub.com&amp;#x2F;case-studies&amp;#x2F;lincoln-labs&amp;#x2F;&lt;/a&gt;</text></item></parent_chain><comment><author>galangalalgol</author><text>People have picked stranger things than julia for safety critical control systems. I know people have generated it from simulink and have used labview, and it wouldn&amp;#x27;t surprise me if somewhere someone is using an excel macro to control the pressure system on a boiler...   The world is a scary place.&lt;p&gt;Reading theough the spark tutorials and examples seems fairly similar to the rustlings excercise. I find the ways spark prevents problems, like forbidding side effects, is more onerous than the borrow checker making me specify a lifetime every so often. I&amp;#x27;m not saying you are wrong to prefer spark, just that people with different backgrounds will find the learning curves different. You have been programming longer than I&amp;#x27;ve been alive, so you certainly have a different perspective. I started with c64 basic then c on the amiga 500, then x86 assembler on 386, them turbo pascal, then turbo c++ on the 386.&lt;p&gt;I can&amp;#x27;t argue that spark isn&amp;#x27;t more mature for formal verification, but it feels like formal verification relies heavily on correct contract specifications with no way to measure when your contracts are correct. Unit tests and coverage at least give me a little feel good that I wrote enough tests for my rust.</text></comment>
<story><title>Welcome to Comprehensive Rust</title><url>https://google.github.io/comprehensive-rust/</url></story><parent_chain><item><author>eggy</author><text>I still play with Rust (and Zig), but I have decided to put my work efforts into SPARK[1], the subset of Ada, for high-integrity software and formal verification. I know AdaCore and Ferrous Systems are collaborating in trying to bring a lot of Ada&amp;#x2F;Spark&amp;#x27;s capabilities to Rust, but this is still going to be some time. Ada has a longer legacy in this game.&lt;p&gt;I am working on safety critical control systems and there is a lot to prune from existing work in this area in SPARK and Ada.&lt;p&gt;This book[2], &amp;quot;Building High Integrity Applications with SPARK&amp;quot; really sold me on the benefits. It is a great intro of how SPARK was used for the CubeSat program at Vermont Technical College (VTC). A CubeSat was successfully launched in 2013. I could not find any critical mission software written in Rust yet especially that far back.&lt;p&gt;I found Julia&amp;#x27;s selection for a flight collision avoidance system perplexing[3], but it proves a PLs syntax and evangelism (maybe not in this case), can bias a selection of a PL for such tasks.
People find Ada&amp;#x2F;SPARK&amp;#x27;s syntax and methods verbose and similar to Pascal or other PLs, however, I was up and running quickly in it as opposed to Rust.&lt;p&gt;You can program to bare metal in SPARK, and the tools are already there to provide high-integrity software. The tools for SPARK automate most of the verification. Most of Rust&amp;#x27;s wishlist is already in SPARK (and Ada). I hope the Ferrous Systems and AdaCore collab bears fruit for Rust, but I have been programming since 1978, and I play with many PLs, but I found Rust&amp;#x27;s initial learning curve very off putting and I don&amp;#x27;t have the time to wait for it to mature to SPARK&amp;#x27;s level. And this is from someone who loves J&amp;#x2F;APL&amp;#x2F;BQN and Lisp, so I have no issue with different programming paradigms. I found Zig much easier to get things done from the start, although it does not strive to be a SPARK or Rust.&lt;p&gt;[1]  &lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;www.adacore.com&amp;#x2F;sparkpro&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;www.adacore.com&amp;#x2F;sparkpro&lt;/a&gt;&lt;p&gt;[2]  &lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;www.amazon.com&amp;#x2F;Building-High-Integrity-Applications-SPARK&amp;#x2F;dp&amp;#x2F;1107040736&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;www.amazon.com&amp;#x2F;Building-High-Integrity-Applications-...&lt;/a&gt;&lt;p&gt;[3]  &lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;juliahub.com&amp;#x2F;case-studies&amp;#x2F;lincoln-labs&amp;#x2F;&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;juliahub.com&amp;#x2F;case-studies&amp;#x2F;lincoln-labs&amp;#x2F;&lt;/a&gt;</text></item></parent_chain><comment><author>brianzelip</author><text>Here’s a recent podcast episode that looks at Rust and Ada with some folks who work on Ada Core, &lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;rustacean-station.org&amp;#x2F;episode&amp;#x2F;067-quentin-ochem-florian-gilcher&amp;#x2F;&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;rustacean-station.org&amp;#x2F;episode&amp;#x2F;067-quentin-ochem-flor...&lt;/a&gt;</text></comment>