Is there any planned support for generating rust code, or for developing a theory that models rust?
As far as I know only F# is planned
but I am not convinced that rust modelisation is possible (or even useful)
Close is Peter Lammich's Isabelle/LLVM that models the LLVM IR semantics (the target of the rust front-end) and you can generate imperative code
but Sepref and co have a significant overhead in learning and implementing
(besides the fact that it is only for imperative non-functional code)
Mathias Fleury said:
but I am not convinced that rust modelisation is possible (or even useful)
It would be nice to be able to prove that rust code is correct. I realise it isn't functional in the haskel sense, but the borrow checker does recover a lot of the safeness of purely functional languages. The rust semantics are quite a bit more constrained than LLVM IR, obviously, so there will be things to be said about rust code (or the sanitised version of it in the compiler) that can't be said about the LLVM IR.
Last updated: Dec 07 2024 at 16:22 UTC