5 ms·

The program cannot be verified against the standard to be correct. There is no standard, how can it be verified.

steveklabnik 3y ago
Because verification does not require a standard. rustc has already been qualified (though not for any aerospace-specific things yet that I'm aware of, but in my understanding the shape is the same) (via Ferrocene[1]), even though there is no Rust Standard. No issues here. 1: https://ferrous-systems.com/blog/qualifying-rust-without-forking/ https://ferrous-systems.com/blog/qualifying-rust-without-for... Also, I don't see where this project claims to be verified.
Xylakant 3y ago
If by "no standard" you mean that there is no language specification for rust, then there is no standard. However, a language specification is not sufficient to verify program correctness, nor is it required. A standard may (and the C standard for example does) leave parts of the behavior as "implementation specific" and there's quite a few edge cases - and that's not even talking about "undefined behavior", of which there is plenty. An even in the behavior that is neither implementation specific nor undefined you'll find enough rope to hang yourself (all the beautiful pointers). There's a reason things such as MISRA C exist - effectively a standard on top of a standard. On the other hand, the rust language - while having no formal spec - is fairly well described, in the form of its RFCs and testsuite. We (the ferrocene team) were able to derive a descriptive specification from the existing description fairly easily. So while there is no ISO standard, and no spec that would be sufficient to write a competing implementation, there is a description of what the language behaves like. You can read up on it at https://spec.ferrocene.dev/ https://spec.ferrocene.dev/ As for verification of correct behavior of such a program, you can employ a host of different techniques depending on what your requirements are - down to verification of the produced bytecode by means of blackbox testing or other.
addaon 3y ago
> There is no standard, how can it be verified. The behavior of the generated binary can be verified against the requirements. Yeah, the most common way to do this is to verify certain properties at the source code level, and then rely on various ways to show equivalence between the source code and the generated assembly, the generated assembly and the generated binary, and the formal semantics of the generated binary and the as-executed semantics on the chosen hardware; but it's perfectly reasonable, and not even particularly unusual, to skip the first equivalence and verify the assembly against the requirements directly.

Because verification does not require a standard. rustc has already been qualified (though not for any aerospace-specific things yet that I'm aware of, but in my understanding the shape is the same) (via Ferrocene[1]), even though there is no Rust Standard. No issues here. 1: https://ferrous-systems.com/blog/qualifying-rust-without-forking/ https://ferrous-systems.com/blog/qualifying-rust-without-for... Also, I don't see where this project claims to be verified.

Xylakant 3y ago

If by "no standard" you mean that there is no language specification for rust, then there is no standard. However, a language specification is not sufficient to verify program correctness, nor is it required. A standard may (and the C standard for example does) leave parts of the behavior as "implementation specific" and there's quite a few edge cases - and that's not even talking about "undefined behavior", of which there is plenty. An even in the behavior that is neither implementation specific nor undefined you'll find enough rope to hang yourself (all the beautiful pointers). There's a reason things such as MISRA C exist - effectively a standard on top of a standard. On the other hand, the rust language - while having no formal spec - is fairly well described, in the form of its RFCs and testsuite. We (the ferrocene team) were able to derive a descriptive specification from the existing description fairly easily. So while there is no ISO standard, and no spec that would be sufficient to write a competing implementation, there is a description of what the language behaves like. You can read up on it at https://spec.ferrocene.dev/ https://spec.ferrocene.dev/ As for verification of correct behavior of such a program, you can employ a host of different techniques depending on what your requirements are - down to verification of the produced bytecode by means of blackbox testing or other.

addaon 3y ago

> There is no standard, how can it be verified. The behavior of the generated binary can be verified against the requirements. Yeah, the most common way to do this is to verify certain properties at the source code level, and then rely on various ways to show equivalence between the source code and the generated assembly, the generated assembly and the generated binary, and the formal semantics of the generated binary and the as-executed semantics on the chosen hardware; but it's perfectly reasonable, and not even particularly unusual, to skip the first equivalence and verify the assembly against the requirements directly.