7 ms·

KRust: A Formal Executable Semantics of Rust

148 points by dmmalam 8y ago

mlazos 8y ago
This is awesome. It also makes me really excited that finally there's a language that's catching on (I consider Haskell, OCaml and the like to be niche) where the subset of the language that is used for a formal semantics is very similar to the language being modeled. I feel like with Javascript, C and other similar languages the core language that is used in a formal semantics has to "patch up" all of the unsafe holes in their respective type systems, and as a result the core language ends up looking a lot different from the language it is intended to model.
- platinumrad 8y ago
  I wouldn't be surprised if the total number of Rust programmers is smaller than the total number of Haskell or OCaml programmers. The latter two are frequently taught in school, unlike Rust.
  - woah 8y ago
    Rust brings some very practical advantages to the table such as portability, performance, safety, and determinism. I wouldn’t be surprised if it’s adoption continues at a much greater rate than Haskell and OCaml which mostly just bring syntax and semantics that many people prefer.
    - platinumrad 8y ago
      If Rust doesn't find its "killer app" I don't see it rapidly growing like Go (network services, containers) or Swift (everything Apple). Widely displacing C is a pipe dream. A more realistic hope is that it will become the wasm language. But if it misses that boat I fear it will remain relatively niche.
      - vvanders 8y ago
        Heh, someone better tell Mozilla that it's time to pack up Firefox and go home then.
        platinumrad 8y ago
        Servo is just one project. How does its existence, or the existence of whatever other components of Firefox that use some amount of Rust, encourage the adoption of Rust by the general programming population? If having a high profile industrial backer makes a language not niche then OCaml is not a niche language. (I wish this were the case.)
        vvanders 8y ago
        What makes you think that the languages which Rust displaces aren't also niche? I used to write a lot of C++, every team I worked on always had a problem finding people who could write native code well, I'm pretty sure that hasn't changed in ~3 years or so. Why does something have to be wildly popular to be considered successful? I've found most of this industry is more about using the right tool for the job then trying to fit one language into every domain space. That said I think there are a few places where you'll see Rust really succeed in the next 3-8 years: 1. Domains that have hard memory or performance constraints. Rust matches C/C++ for performance(and I say this as a hardcore C++ perf nut) but without the segfaults/corruption(unless you step into unsafe land). 2. Products that need to go to multiple platforms but can't afford a GC. Rust has by far the best cross-platform development story I've seen in a natively compiled language. I've personally build things that run on WASM/Win32/OSX/Android/Linux across a wide range of hardware and embedded in C#/Java/C++/C. 3. Places where safety/memory corruption is unacceptable. You just get less of these from Rust, full stop. Yes you can do it in C/C++ but you better be willing to have a QA org larger than your dev team. Firefox is a perfect example of how these various concerns intersect. I used to be a serious C++ developer working on high performance, memory constrained platforms. In the past two years anything green field for me has been Rust based and I've been 100% satisfied. In both personal projects and some professional work Rust has never come up short. Is it hard to write? Sure. Do I spend less time debugging/tracking down mem corruption/dealing with poor ownership? Hell yeah.
  - lambda 8y ago
    Rust is increasingly frequently taught in schools; and when Haskell or OCaml are taught in schools, it's usually as part of a "programming languages" survey course where you learn a little bit of a few languages of different paradigms, and I expect that most students won't really retain much from the class a year or two later unless it helped them develop an independent interest in functional programming.
    - jononor 8y ago
      Can you link to one or two classes taught in Rust? It is surprising to me, since academia often trails by many years.
      - iuppiter 8y ago
        http://cis198-2016s.github.io/ http://cis198-2016s.github.io/
        jononor 8y ago
        Not taught since fall 2016. Was taught by some passionate students it looks like. Only current one I could find is https://www.mccormick.northwestern.edu/eecs/courses/descriptions/396-496-9.html https://www.mccormick.northwestern.edu/eecs/courses/descript...
      - steveklabnik 8y ago
        There’s been a few over the years, one of the first was an OS class before Rust 1.0. As you’ve mentioned downthread, sometimes they stick with it, sometimes they don’t. Often classes that are run by grad students or adjuncts change when the teachers change. Two classes off the top of my head from this spring: https://www.cs.umd.edu/class/spring2018/cmsc330/ https://www.cs.umd.edu/class/spring2018/cmsc330/ https://web.stanford.edu/class/cs140e/assignments/0-blinky/ https://web.stanford.edu/class/cs140e/assignments/0-blinky/ Hearing rumbles of some more in the future...
    - samth 8y ago
      This is accurate about the US -- in Europe things are quite different. Haskell is regularly taught in first programming courses in the UK, for example, and OCaml is very widely taught in France.
  - staticassertion 8y ago
    Almost certainly, yes. And lots of big companies use Haskell, just like Rust - Facebook has used it for a while now. It's important to remember that while rust may dominate the HN headlines, it's still a very niche language. That said, it's also showing a lot of promise in a world that largely dismisses programming languages as being irrelevant.
  - pornel 8y ago
    In Open Source (at least in the sample measured by that site) number of people writing Rust has outgrown Haskell and OCaml, and is approaching popularity of Scala: https://www.openhub.net/languages/compare?utf8=%E2%9C%93&measure=contributors&language_name%5B%5D=haskell&language_name%5B%5D=ocaml&language_name%5B%5D=rust&language_name%5B%5D=scala&language_name%5B%5D=-1 https://www.openhub.net/languages/compare?utf8=%E2%9C%93&mea...
  - adamnemecek 8y ago
    The two are ~20 years older than Rust. However Rust is super mature for it's age.
  - coldtea 8y ago
    Rust has more momentum and visibility -- and seems poised to have more uptake in startups and industry. Already several major companies use it -- https://www.rust-lang.org/en-US/friends.html https://www.rust-lang.org/en-US/friends.html For Haskell, the best I've heard is Facebook for some custom dev tools and Standard Chartered. I'm sure there's more, but...
kibwen 8y ago
At the recent Rust All-Hands in Berlin a few groups of researchers independently working on verifying Rust's semantics decided to form a working group to focus their efforts (see the official announcement at https://internals.rust-lang.org/t/announcing-the-formal-verification-working-group/7240 https://internals.rust-lang.org/t/announcing-the-formal-veri... ). I don't recognize any of the names on this paper from there, so it looks like there may be even more people working on this than we thought, and if that also happens to encompass anyone reading this comment, feel free to reach out to the working group. :) Regarding the OP, I'll quote a comment from reddit: https://www.reddit.com/r/rust/comments/8g6mam/krust_a_formal_executable_semantics_of_rust/ https://www.reddit.com/r/rust/comments/8g6mam/krust_a_formal... "It looks like they wrote an interpreter for a small subset of Rust in a particular formal system. But the subset is extremely small, and it doesn't look like they derived any novel results from this. The examples they give, of proving the running time of a GCD algorithm, would work in pretty much any procedural language; it's pretty much just a syntax modification away from the same example in any language. They implement a very simple model of borrow checking, but their subset doesn't seem to support references in type signatures, so it doesn't seem like they can even model any inter-procedural effects of the borrow checker, just some purely local restrictions on aliasing. I suppose that this is a good first step if you want to write a formal semantics of Rust in 𝕂, but it seems like there's not really enough here yet to be of interest."
- still_grokking 8y ago
  > "I suppose that this is a good first step if you want to write a formal semantics of Rust in 𝕂, but it seems like there's not really enough here yet to be of interest." I thing the work is interesting. It would be a great endeavor to model the whole language so you need people to help with that. But how would one know that someone has started a project like that if they don't publish something about it? In my opinion the whole story about only accepting "novel" and "readily applicable" results in academia isn't quite helpful. A "Publish early, publish often" strategy could produce more and better results in the long term I think. If a result isn't useful or novel on it's own that's no issue imo. It can still become an important building block of some later innovation! Reusable work done is work done, indifferently of it's "novelty" or direct applicability. Also the 𝕂 Framework is amazing for formal reasoning about languages so this work is indeed an important first step.
bitmadness 8y ago
The abstract of this paper is written in very poor English. I encourage the authors to have a native speaker proofread their paper.
nickpsecurity 8y ago
This is the same underlying tool that powers KCC and RVMatch. https://github.com/kframework/c-semantics https://github.com/kframework/c-semantics https://runtimeverification.com/match/ https://runtimeverification.com/match/ Exactly what I’d hoped someone would do. Well, the first step anyway. The second step was doing a Rust semantics in terms of the C semantics already done. That allows quite a few things like Rust-to-C compilers, defeating Karger-Thompson attack, and potentially verification of interactions of Rust and C FFI code. On my end down the line, also use of C tooling for verification of equivalent Rust code.
deleted 8y ago
[deleted]
iuppiter 8y ago
I am the author of this paper. The semantics is far from complete and I am still working it. It is not a easy to formalize Rust completely. KRust is now just very very small step towards that. It may be not "useful" currently, but I think there will be a complete one if more people work on this.
- tom_mellior 8y ago
  As a small but I think important remark, the statement in the abstract that you tested on the "official Rust test suite" is very misleading. As the text later makes clear, you tested on a small fragment of it. That is good, that is important, and you should continue doing it. But as phrased in the abstract, I first though that you pass all of the Rust tests, or at least a significant majority of them. If I were a reviewer of this paper, I would complain about this loudly, including to the PC chair/editor. As a fellow researcher, I urge you to change this wording in the abstract to something less misleading.
  - iuppiter 8y ago
    Thank you for pointing it out. I just used all the codes in the official test suite to test KRust, but it only passed a small fragment.
- pornel 8y ago
  Thank you for working on it!

148 points by dmmalam 8y ago

This is awesome. It also makes me really excited that finally there's a language that's catching on (I consider Haskell, OCaml and the like to be niche) where the subset of the language that is used for a formal semantics is very similar to the language being modeled. I feel like with Javascript, C and other similar languages the core language that is used in a formal semantics has to "patch up" all of the unsafe holes in their respective type systems, and as a result the core language ends up looking a lot different from the language it is intended to model.

platinumrad 8y ago
I wouldn't be surprised if the total number of Rust programmers is smaller than the total number of Haskell or OCaml programmers. The latter two are frequently taught in school, unlike Rust.
- woah 8y ago
  Rust brings some very practical advantages to the table such as portability, performance, safety, and determinism. I wouldn’t be surprised if it’s adoption continues at a much greater rate than Haskell and OCaml which mostly just bring syntax and semantics that many people prefer.
  - platinumrad 8y ago
    If Rust doesn't find its "killer app" I don't see it rapidly growing like Go (network services, containers) or Swift (everything Apple). Widely displacing C is a pipe dream. A more realistic hope is that it will become the wasm language. But if it misses that boat I fear it will remain relatively niche.
    - vvanders 8y ago
      Heh, someone better tell Mozilla that it's time to pack up Firefox and go home then.
      - platinumrad 8y ago
        Servo is just one project. How does its existence, or the existence of whatever other components of Firefox that use some amount of Rust, encourage the adoption of Rust by the general programming population? If having a high profile industrial backer makes a language not niche then OCaml is not a niche language. (I wish this were the case.)
        vvanders 8y ago
        What makes you think that the languages which Rust displaces aren't also niche? I used to write a lot of C++, every team I worked on always had a problem finding people who could write native code well, I'm pretty sure that hasn't changed in ~3 years or so. Why does something have to be wildly popular to be considered successful? I've found most of this industry is more about using the right tool for the job then trying to fit one language into every domain space. That said I think there are a few places where you'll see Rust really succeed in the next 3-8 years: 1. Domains that have hard memory or performance constraints. Rust matches C/C++ for performance(and I say this as a hardcore C++ perf nut) but without the segfaults/corruption(unless you step into unsafe land). 2. Products that need to go to multiple platforms but can't afford a GC. Rust has by far the best cross-platform development story I've seen in a natively compiled language. I've personally build things that run on WASM/Win32/OSX/Android/Linux across a wide range of hardware and embedded in C#/Java/C++/C. 3. Places where safety/memory corruption is unacceptable. You just get less of these from Rust, full stop. Yes you can do it in C/C++ but you better be willing to have a QA org larger than your dev team. Firefox is a perfect example of how these various concerns intersect. I used to be a serious C++ developer working on high performance, memory constrained platforms. In the past two years anything green field for me has been Rust based and I've been 100% satisfied. In both personal projects and some professional work Rust has never come up short. Is it hard to write? Sure. Do I spend less time debugging/tracking down mem corruption/dealing with poor ownership? Hell yeah.
- lambda 8y ago
  Rust is increasingly frequently taught in schools; and when Haskell or OCaml are taught in schools, it's usually as part of a "programming languages" survey course where you learn a little bit of a few languages of different paradigms, and I expect that most students won't really retain much from the class a year or two later unless it helped them develop an independent interest in functional programming.
  - jononor 8y ago
    Can you link to one or two classes taught in Rust? It is surprising to me, since academia often trails by many years.
    - iuppiter 8y ago
      http://cis198-2016s.github.io/ http://cis198-2016s.github.io/
      - jononor 8y ago
        Not taught since fall 2016. Was taught by some passionate students it looks like. Only current one I could find is https://www.mccormick.northwestern.edu/eecs/courses/descriptions/396-496-9.html https://www.mccormick.northwestern.edu/eecs/courses/descript...
    - steveklabnik 8y ago
      There’s been a few over the years, one of the first was an OS class before Rust 1.0. As you’ve mentioned downthread, sometimes they stick with it, sometimes they don’t. Often classes that are run by grad students or adjuncts change when the teachers change. Two classes off the top of my head from this spring: https://www.cs.umd.edu/class/spring2018/cmsc330/ https://www.cs.umd.edu/class/spring2018/cmsc330/ https://web.stanford.edu/class/cs140e/assignments/0-blinky/ https://web.stanford.edu/class/cs140e/assignments/0-blinky/ Hearing rumbles of some more in the future...
  - samth 8y ago
    This is accurate about the US -- in Europe things are quite different. Haskell is regularly taught in first programming courses in the UK, for example, and OCaml is very widely taught in France.
- staticassertion 8y ago
  Almost certainly, yes. And lots of big companies use Haskell, just like Rust - Facebook has used it for a while now. It's important to remember that while rust may dominate the HN headlines, it's still a very niche language. That said, it's also showing a lot of promise in a world that largely dismisses programming languages as being irrelevant.
- pornel 8y ago
  In Open Source (at least in the sample measured by that site) number of people writing Rust has outgrown Haskell and OCaml, and is approaching popularity of Scala: https://www.openhub.net/languages/compare?utf8=%E2%9C%93&measure=contributors&language_name%5B%5D=haskell&language_name%5B%5D=ocaml&language_name%5B%5D=rust&language_name%5B%5D=scala&language_name%5B%5D=-1 https://www.openhub.net/languages/compare?utf8=%E2%9C%93&mea...
- adamnemecek 8y ago
  The two are ~20 years older than Rust. However Rust is super mature for it's age.
- coldtea 8y ago
  Rust has more momentum and visibility -- and seems poised to have more uptake in startups and industry. Already several major companies use it -- https://www.rust-lang.org/en-US/friends.html https://www.rust-lang.org/en-US/friends.html For Haskell, the best I've heard is Facebook for some custom dev tools and Standard Chartered. I'm sure there's more, but...

kibwen 8y ago

At the recent Rust All-Hands in Berlin a few groups of researchers independently working on verifying Rust's semantics decided to form a working group to focus their efforts (see the official announcement at https://internals.rust-lang.org/t/announcing-the-formal-verification-working-group/7240 https://internals.rust-lang.org/t/announcing-the-formal-veri... ). I don't recognize any of the names on this paper from there, so it looks like there may be even more people working on this than we thought, and if that also happens to encompass anyone reading this comment, feel free to reach out to the working group. :) Regarding the OP, I'll quote a comment from reddit: https://www.reddit.com/r/rust/comments/8g6mam/krust_a_formal_executable_semantics_of_rust/ https://www.reddit.com/r/rust/comments/8g6mam/krust_a_formal... "It looks like they wrote an interpreter for a small subset of Rust in a particular formal system. But the subset is extremely small, and it doesn't look like they derived any novel results from this. The examples they give, of proving the running time of a GCD algorithm, would work in pretty much any procedural language; it's pretty much just a syntax modification away from the same example in any language. They implement a very simple model of borrow checking, but their subset doesn't seem to support references in type signatures, so it doesn't seem like they can even model any inter-procedural effects of the borrow checker, just some purely local restrictions on aliasing. I suppose that this is a good first step if you want to write a formal semantics of Rust in 𝕂, but it seems like there's not really enough here yet to be of interest."

still_grokking 8y ago
> "I suppose that this is a good first step if you want to write a formal semantics of Rust in 𝕂, but it seems like there's not really enough here yet to be of interest." I thing the work is interesting. It would be a great endeavor to model the whole language so you need people to help with that. But how would one know that someone has started a project like that if they don't publish something about it? In my opinion the whole story about only accepting "novel" and "readily applicable" results in academia isn't quite helpful. A "Publish early, publish often" strategy could produce more and better results in the long term I think. If a result isn't useful or novel on it's own that's no issue imo. It can still become an important building block of some later innovation! Reusable work done is work done, indifferently of it's "novelty" or direct applicability. Also the 𝕂 Framework is amazing for formal reasoning about languages so this work is indeed an important first step.

bitmadness 8y ago

The abstract of this paper is written in very poor English. I encourage the authors to have a native speaker proofread their paper.

nickpsecurity 8y ago

This is the same underlying tool that powers KCC and RVMatch. https://github.com/kframework/c-semantics https://github.com/kframework/c-semantics https://runtimeverification.com/match/ https://runtimeverification.com/match/ Exactly what I’d hoped someone would do. Well, the first step anyway. The second step was doing a Rust semantics in terms of the C semantics already done. That allows quite a few things like Rust-to-C compilers, defeating Karger-Thompson attack, and potentially verification of interactions of Rust and C FFI code. On my end down the line, also use of C tooling for verification of equivalent Rust code.

deleted 8y ago

[deleted]

iuppiter 8y ago

I am the author of this paper. The semantics is far from complete and I am still working it. It is not a easy to formalize Rust completely. KRust is now just very very small step towards that. It may be not "useful" currently, but I think there will be a complete one if more people work on this.

tom_mellior 8y ago
As a small but I think important remark, the statement in the abstract that you tested on the "official Rust test suite" is very misleading. As the text later makes clear, you tested on a small fragment of it. That is good, that is important, and you should continue doing it. But as phrased in the abstract, I first though that you pass all of the Rust tests, or at least a significant majority of them. If I were a reviewer of this paper, I would complain about this loudly, including to the PC chair/editor. As a fellow researcher, I urge you to change this wording in the abstract to something less misleading.
- iuppiter 8y ago
  Thank you for pointing it out. I just used all the codes in the official test suite to test KRust, but it only passed a small fragment.
pornel 8y ago
Thank you for working on it!