Questions on proof assistants

[Freek Wiedijk]

Dear Tim,

>When it comes to ordinary software, it is routine practice
>to completely discard old code and start afresh.

Formalization is much more like programming than many like.

When you want an operating system written in Rust, do you
fully automatically convert the Linux source code to Rust?
No.  But do people routinely completely discard the Linux
source code all the time and start afresh?  No.

So with formal proofs it's like that.

Freek