advent_of_code VS misra-rust

I've updated the README file of my github repository where I have put solutions to Advent of Code. The README file outlines my thoughts and considerations when writing the code which uses a minimal subset of the full Ada language, uses AdaControl to know the intended subset is used, how memory safety and resource management in general has been done when not taking advantage of SPARK. https://github.com/joakim-strandberg/advent_of_code

I am aware that controlled types are associated with performance penalty although I haven't fully understood why. When I write Ada code I try to avoid using them although sometimes there seem to be no workaround like for example when using Gautier's multi precision integer implementation when doing Advent of Code 2021 (https://github.com/joakim-strandberg/advent_of_code, the "Big_Int_Holder" package in advent_of_code_2021.adb). Return value optimization (RVO) does make me think of extended return and limited types in Ada 2005, although as was discussed in the video that move semantics is more than that. Thanks for bringing up the subject!

It's kind of the opposite for me. It takes much less time to understand what Ada-written code is doing compared to any of the C-type languages, or even Rust. It is very plainly written. Verbose, yes, but much more plainly written.

Just take a look at this, and tell me it's not legible: https://github.com/joakim-strandberg/advent_of_code/blob/mas...

Ada95, part one (full code at https://github.com/joakim-strandberg/advent_of_code/):

Ouch, link doesn't work, due to escape characters. The proper link: https://github.com/joakim-strandberg/advent_of_code

MISRA and Ferrocene are not really related.

MISRA is, as you say, a set of rules for writing C code, that restrict what you can do.

Ferrocene is a qualified compiler. You write any normal Rust code you want: it's still the upstream Rust compiler. There are no restrictions.

Incidentally, someone has compared what MISRA does to what Rust does: https://github.com/PolySync/misra-rust/blob/master/MISRA-Rul...

Given that they can't repeat the MISRA stuff there, it's a bit disjoined, but it sure is interesting!

A fun github repo: "what would MISRA look like applied to Rust" https://github.com/PolySync/misra-rust/blob/master/MISRA-Rul...

(They're comparing with the C version, not the C++ version...)

> There are huge swathes of MISRA which forbid things which not only aren't possible in Rust or SPARK

I can't vouch for its accuracy, but https://github.com/PolySync/misra-rust

When it comes to MISRA C, it is interesting to note how many (a majority) of its rules do not apply or have native enforcement[1].

You might have also seen the AUTOSTAR Rust in Automotive Working Group announcement recently[2].

[1]: https://github.com/PolySync/misra-rust/blob/master/MISRA-Rul...

[2]: for some reason the announcement was removed from the "News and events" site, https://webcache.googleusercontent.com/search?q=cache%3Ahttp... but it is still available as a PDF https://www.autosar.org/fileadmin/user_upload/20220308_RustW...

There's actually already a comparison: https://github.com/PolySync/misra-rust/blob/master/MISRA-Rules.md

Rust makes quite a few things more rigorous (e.g. pairing allocations with deallocations and reference validity). It basically fulfills the job of a static analyzer baked into the language.

It's also a vastly more analyzable language (in that its syntax is reasonably unambiguous and there's no dynamic runtime in play) and it can be integrated well.

Toolchain quality (error reporting, built in testing, awareness of primitives like "libraries", etc.) is also a huge strong point.

We're reasonably confident that we can use safe Rust as is, with strong guidance on how to do unsafe Rust.

For a tangible investigation of that space, PolySync has a project that has a look at MISRA rules from a Rust perspective. https://github.com/PolySync/misra-rust/blob/master/MISRA-Rul...

Ada is a good example here: the language has not evolved something like MISRA-C (it has evolved SPARK for formal verification, but I see that differently).