Matthew Pocock (Aug 31 2023 at 18:49): Matthew Pocock (Aug 31 2023 at 18:49):Is there any planned support for generating rust code, or for developing a theory that models rust?
Mathias Fleury (Aug 31 2023 at 19:09):As far as I know only F# is planned
Mathias Fleury (Aug 31 2023 at 19:09):but I am not convinced that rust modelisation is possible (or even useful)
Mathias Fleury (Aug 31 2023 at 19:10):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
Mathias Fleury (Aug 31 2023 at 19:11):but Sepref and co have a significant overhead in learning and implementing
Mathias Fleury (Aug 31 2023 at 19:12):(besides the fact that it is only for imperative non-functional code)
Matthew Pocock (Aug 31 2023 at 20:19):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: May 02 2024 at 08:19 UTC