Hi, Ilmārs --
One of the things we're hoping to do is a type safety proof for a
subset of Rust. Because machine-checked proofs are so labor-intensive
(and it's almost impossible to appreciate just how labor-intensive
until you try a proof for an even slightly realistic language), the
usual approac
Greetings!
(I hope this isn't spam.)
I am bachelor's degree student (the first of four years) in Computer
Sciences. I am searching for any ideas that can be used as a research topic
and is both related to Rust and formal verification/specification or
similar.
I'm learning Coq already, so it's my
