Comment by nullc

Comment by nullc 10 months ago

> but it could just as well be ported to Rust

Without formal semantics for the complete rust language the result couldn't be verified. Rust's complexity makes it hard to define formal semantics.

I wouldn't normally bring this up as a disadvantage of rust, but people aren't normally talking about software that has been formally verified.

junon 10 months ago

Check out ferrocene.

wahern 10 months ago

Ferrocene doesn't involve formal proofs. ISO 26262 and IEC 61508 are primarily process-focused standards for project management, quality control, integration, testing, and code review. To the extent there's automated code analysis, it would involve linting for disallowed patterns similar to MISRA C.

Reply View | 0 replies