Ferrocene for Hubris?

[ghost]

Would it be possible to put the existing Hubris (Rust) codebase through Ferrocene?

And, maybe, in the future, setup some mechanism for changes to be passed through Ferrocene before being accepted in!

Maybe, just maybe, Hubris might end-up becoming the new standard for mission critical systems in medical devices and aerospace & defense equipment.

[steveklabnik]

What do you mean by putting it "through" Ferrocene, exactly?

[ghost]

Hi @steveklabnik.

Ferrocene is to Rust as the combination of Ada/SPARK compiler and GNATProve is to Ada/SPARK.

When a Rust project is compiled using Ferrocene (instead of the usual Rust LLVM toolchain), the code is verified for high-integrity.
I would suggest that you consider taking a look at the GNATProve tool from AdaCore, as at the moment Ferrocene is not ready.
Using GNATProve will give you a good idea about the ways in which verification works.

BTW, @steveklabnik, it is good to see you here. I am that same guy for whom you had worked (for free) to translate that purely symbolic Lisp interpreter from ANSI-C to Rust (probably using some online tool).

Cheers.

[steveklabnik]

I am not aware of Ferrocene having a theorem prover, only producing a verified compiler. Given that it's intended to specify what rustc does, I don't see the advantage of purchasing Ferrocene, given that it would only check off a box that we aren't required to have used to ship the product.

[ghost]

Just a verified compiler can't be enough to emit software for mission critical systems, as has been advertised by AdaCore.

I am not an employee of Oxide Computer, and hence I cannot communicate with AdaCore from a position of authority.
Would you be willing to post queries to AdaCore? They would be able to answer your queries well.