Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Porting a Haskell graphics framework to Rust

phaazon.blogspot.com

Post reply on HN
Print view View original

11–18 of 18 posts

Re: Porting a Haskell graphics framework to Rust

#11

Post by steveklabnik »

eddyb wrote: post #7
steveklabnik wrote: post #5

Earlier 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).

They say it a few different ways on their site. Regardless, it's research, so we'll see if they even figure it out! I hope so, though.

Re: Porting a Haskell graphics framework to Rust

#12

Post by cwzwarich »

nickpsecurity wrote: post #9
eddyb wrote: post #7

Earlier quoted context omitted.

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 sa…

The fundamental problem is that Rust is actually two languages that interact with each other. There is the high-level language with a region system, traits, etc. as well as the low-level language used for unsafe code, which exposes most of the functionality and memory model of LLVM IR (which is very C-like).

Formalizing the high-level language would have some difficulties, e.g. the trait system has a lot of ad-hoc complexity, and there are convenience features like automatic destructors that improve programmer productivity but greatly complicate the definition of things like evaluation order (which is currently undefined for Rust). These things make the specification more complex, but they appear to be well within the limits of current programming language technology. For example, the safe subset of Rust could possibly be translated into a relatively standard type system with linear regions, e.g. http://www.cs.cornell.edu/people/fluet/research/substruct-re....

The difficulty comes at the semantic boundary, where the state-of-the-art in modeling the interaction between distinct languages is still far away from the safe / unsafe portions of Rust. This is an interesting research project, and fits in well with a general trend of cross-language interaction that appears in current research on programming language formalization. However, because it requires formalizing something that includes a C-like language, it's hard to imagine it ever being any simpler than formalizing a C-like language. If you're a user of unsafe code and just want to prove that the unsafe code is "memory-safe" (a somewhat nebulous term), then this helps you out. But if you're going to prove that your entire program is correct, why bother with all of the extra complexity?

Re: Porting a Haskell graphics framework to Rust

#13

Post by nickpsecurity »

cwzwarich wrote: post #12
nickpsecurity wrote: post #9

Earlier quoted context omitted.

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 sa…

The fundamental problem is that Rust is actually two languages that interact with each other. There is the high-level language with a region system, traits, etc. as well as the low-level language used for unsafe code, which exposes most of the functionality and memory model of LLVM IR (which is very C-like). Formalizing the high-level language would have some difficulties, e.g. the trait system has a lot of ad-hoc co…

Thanks for insightful reply. The difficulties make more sense now. Far as why at the end, the guarantees formal verification give you can far exceed basic, memory safety for common usage. That's why for many verification projects.

Re: Porting a Haskell graphics framework to Rust

#14

Post by cwzwarich »

nickpsecurity wrote: post #13
cwzwarich wrote: post #12

Earlier quoted context omitted.

The fundamental problem is that Rust is actually two languages that interact with each other. There is the high-level language with a region system, traits, etc. as well as the low-level language used for unsafe code, which exposes most of the functionality and memory model of LLVM IR (which is very C-like). Formalizing the high-level language would have some difficulties, e.g. the trait system has a lot of ad-hoc co…

Thanks for insightful reply. The difficulties make more sense now. Far as why at the end, the guarantees formal verification give you can far exceed basic, memory safety for common usage. That's why for many verification projects.

To clarify: I was rhetorically asking why one would bother with the complexity of completely verifying a program in Rust rather than C, not why one would want full verification rather than memory safety.

Re: Porting a Haskell graphics framework to Rust

#15

Post by nickpsecurity »

cwzwarich wrote: post #14
nickpsecurity wrote: post #13

Earlier quoted context omitted.

Thanks for insightful reply. The difficulties make more sense now. Far as why at the end, the guarantees formal verification give you can far exceed basic, memory safety for common usage. That's why for many verification projects.

To clarify: I was rhetorically asking why one would bother with the complexity of completely verifying a program in Rust rather than C, not why one would want full verification rather than memory safety.

(a) The program had to be written in Rust as part of a whole application or for seemless interoperability

(b) You wanted to avoid problems of C. Opposed to it in general with Rust an option.

(c) Your hardware architecture easily supported Rust's safe subset but not C's model. Examples include Burroughs, Ten15, Java CPU, and SAFE (crash-safe.org) CPU's. Edit to say may as I'm not a Rust programmer. C being very unconstrained breaks most of these models.

(d) Others have proven precedents but this is speculative: doing a split between formal verification and type system for safety. A number of projects have done this. A simplifying example is that you model check or verify an abstract design that you code a Rust equivalent to. The semantics helps with the abstraction that knocks out A, B, and C classes of problems. The proven type system of Rust (or SPARK or whatever) is leveraged for X, Y, and Z problem classes. Each method is applied where it's strong.

These are best a quick brainstorm can do at this hour for me. :)

Re: Porting a Haskell graphics framework to Rust

#16

Post by vvanders »

steveklabnik wrote: post #6
vvanders wrote: post #3

Earlier quoted context omitted.

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.

That sounds nice, I spent a good chunk of today hacking on a FRP implementation similar to Elm and the ability to not clone + a few other things around closures kept painting me into a corner each time. I even went as far to drop down to std::mem::transmute_copy, but when I hit a Box B> the type has already been erased and I can't recover it.

It seems like if you have no references in your closure you should be able to pass them around as a value-type(with generics, of course). From what I can tell without that there's a whole range of FP patterns that just aren't representable in Rust because of it.

Re: Porting a Haskell graphics framework to Rust

#17

Post by dbaupp »

vvanders wrote: post #3
nickpsecurity wrote: post #2

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 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…

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 ...>` 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.

Re: Porting a Haskell graphics framework to Rust

#18

Post by vvanders »

dbaupp wrote: post #17
vvanders wrote: post #3

Earlier quoted context omitted.

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…

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 ...>` 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…

Duh, dunno why I'd forgotten Rc.

I'm still not a huge fan of the extra allocation(and chance for cycles) but I stand corrected that it does work, kudos.

Post reply on HN