Stream: General

Topic: Rust


view this post on Zulip 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?

view this post on Zulip Mathias Fleury (Aug 31 2023 at 19:09):

As far as I know only F# is planned

view this post on Zulip Mathias Fleury (Aug 31 2023 at 19:09):

but I am not convinced that rust modelisation is possible (or even useful)

view this post on Zulip 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

view this post on Zulip Mathias Fleury (Aug 31 2023 at 19:11):

but Sepref and co have a significant overhead in learning and implementing

view this post on Zulip Mathias Fleury (Aug 31 2023 at 19:12):

(besides the fact that it is only for imperative non-functional code)

view this post on Zulip 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: Dec 07 2024 at 16:22 UTC