Porting a Haskell graphics framework to Rust

Porting a Haskell graphics framework to Rust(phaazon.blogspot.com)

57 points by chiachun 10 years ago | 17 comments

Fascinating that a Haskell tool mapped so well to Rust. Might make it easier to do seL4-style developments with Rust given they simultaneously do a Haskell model and C code w/ equivalence proof. A Haskell subset that uses whatever verification & testing tools they have might be extracted to an equivalent Rust program automatically or with manual guidance. The assertions or tests would be extracted for equivalence testing. That might have significant safety and maintenance benefit even without HOL parts.

What do the Rust people think of that idea? And how hard would you guess an AutoCorres-style tool be for it vs C in event we wanted HOL parts?

cwzwarich 10 years ago | |

Ironically, it is probably easier to write tooling for verifying C code than it is for verifying Rust code. And the additional benefits of Rust also don't help you that much if you're going to be verifying things; whatever memory safety is provided by Rust would fall out of general correctness.

For C, you just need to come up with a restricted semantics for a subset of C (e.g. you can pick a particular evaluation order, assuming your implementation also respects it). Rust is a much more complex language, with no formal semantics forthcoming, and you would need to verify the semantic properties supposedly enforced by the type system, as well as their interaction with unsafe code. All of this would require new deep research, whereas the equivalent for C-like languages is well-trodden ground by now.

steveklabnik 10 years ago | | |

> with no forms semantics forthcoming

Actually, €5MM grant has been given to some academics to produce a formal model of Rust over the next few years. So we'll see... A big part of it is also formalizing what unsafe means, which is the hard part.

nickpsecurity 10 years ago | | |

"Rust is a much more complex language, with no formal semantics forthcoming" "All of this would require new deep research"

That's what my Googling showed me. Good call. SPARK, C subsets, and embedded Java still winning in this area.

vvanders 10 years ago | |

The one thing that's tripping me up on Rust from doing everthing in a purely functional way is the way closures are dealt with. I really hate the idea that I'm going to need to Box::new() every closure I pass around if I want to return it from a function or store it. Even simple move closures can't be cloned and makes some things that are simple in Haskell/Elm/etc much more painful.

Don't get me wrong, great language but I'm a but dubious of the 1:1 porting story here.

dbaupp 10 years ago | | |

Closures in other languages like Haskell, JavaScript and Python (and almost certainly Elm too, I've never used it and hence don't know for sure) are similar to the `Rc<Fn(...) -> ...>` type in Rust. In fact, if absolutely necessary, one could probably use that everywhere.

Stuff like this is one of the trade-offs in Rust: control over exactly how closures behave (if allocations are necessary, if virtual calls are necessary when calling it) is balanced with/detracts from how much typing one needs to do to get them to work.

cm3 10 years ago | | |

My number one gripe is missing TCO because I find writing recursive functions more natural for many problems. We can't have everything.

steveklabnik 10 years ago | | |

There's an RFC being actively worked on that will make it easier to pass around unboxed closures.