Porting a Haskell graphics framework to Rust
phaazon.blogspot.com
Porting a Haskell graphics framework to Rust
1–10 of 18 posts
Re: Porting a Haskell graphics framework to Rust
#2Fascinating 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?
Re: Porting a Haskell graphics framework to Rust
#3Fascinating 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 tes…
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.
Re: Porting a Haskell graphics framework to Rust
#4Fascinating 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 tes…
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.
Re: Porting a Haskell graphics framework to Rust
#5Fascinating 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 tes…
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 ord…
> 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.
Re: Porting a Haskell graphics framework to Rust
#6Fascinating 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 tes…
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…
There's an RFC being actively worked on that will make it easier to pass around unboxed closures.
Re: Porting a Haskell graphics framework to Rust
#7Earlier quoted context omitted.
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 ord…
> 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.
My understanding was that the goal of that research project is to produce tools for proving code written in unsafe Rust as safe at the API boundary (with limitations around FFI and inline assembly, of course).
Re: Porting a Haskell graphics framework to Rust
#8Fascinating 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 tes…
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…
My number one gripe is missing TCO because I find writing recursive functions more natural for many problems. We can't have everything.
Re: Porting a Haskell graphics framework to Rust
#9Earlier quoted context omitted.
> 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.
My understanding was that the goal of that research project is to produce tools for proving code written in unsafe Rust as safe at the API boundary (with limitations around FFI and inline assembly, of course).
I found two:
ftp://ftp.cs.washington.edu/tr/2015/03/UW-CSE-15-03-02.pdf
http://plv.mpi-sws.org/rustbelt/#project
The first formalized the safety-critical parts of the language to show them sound when used with safety on. The second will try to do that with unsafe. Nobody seems to be working on a full, formal semantics. That's disturbing given how many problems they tend to catch. So, SPARK/Ada combo still leads in safety for now.
Gave myself the idea that maybe someone can formalize a super/subset of Rust much like SPARK for Ada. Code most critical stuff in it with it just becoming functions other Rust code called. My original idea is possible at that point given complexity is minimized.
EDIT: Just finished skimming the first then reading conclusion in detail. It's apparently not Rust's model itself so much as a similar one named Patina that still has to map to the real thing. That's when the problems will show up. Also, Rust type system was updated several times while they were doing all that.
Re: Porting a Haskell graphics framework to Rust
#10Fascinating 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 tes…
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 ord…
"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.