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-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. :)
"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."
> "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.
> A "Publish early, publish often" strategy could produce more and better results in the long term I think.
That (at least the "publish early" part) is already the case for a lot of programming language research in things like semantics or program analysis. Published papers often treat a toy language (no arrays, no dynamic memory allocation, etc.) and leave the rest for "future work". Sometimes that future work does materialize, often it doesn't.
It's a difficult situation for academia: If the basic system is too hard to extend to a full language, you will end up without final results, and from the point of view of your funders you have just wasted a lot of time and money. If it's too easy to extend to a realistic language, you might build a tool but end up doing "only engineering" without having new breakthroughs to publish, again seen in academia as wasting research funds.
For many people in academia, the incentives for building systems really applicable to real-world languages are just not there.
It's a long, hard way from a research prototype to something that works on a machine different from the author's laptop. It's unclear whether paying researchers to build actual products makes sense. If there is a clear market for the application, there is always the possibility to start a spin-off company.
Sure, but there are many many useful tools for which there is no clear market. I do think academic institutions should do more to value and promote development of useful artifacts. But that's difficult to do if rankings (of people and of institutions) are only based on academic publications, which (for the most part) don't include tool descriptions.
> 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.
I fail to see how publishing repeats of the same old conclusions that boil down to applying the same basic and well-known techniques to specific subsets of a trendy programming language, and in the process failing to provide anything meaningful, does anything to advance science.
In fact, what does the article add to the understanding of the problem?
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.
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.
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.
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:
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.
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.
There's nothing about Go that makes it particularly good for containers. It actually requires some ugly hacks in C to make it handle namespaces correctly (because namespaces are configured per-thread, and Go decides to spawn new threads somewhat arbitrarily which is not visible to the program).
If rust continues to improve ergonomics and library support, I don't see anything stopping it from replacing C except in niche embedded systems that don't get LLVM support.
Correct, but it does mean that those of us not so found of Go, have to actually use it when dealing with Docker and K8s deployment scenarios, where devops are keen in using it as their tool of choice.
Trying to avoid Go in such scenarios is a futility.
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.)
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?
I think Rust does need to aim for strong mainstream acceptance. As I'm sure you've experienced, lower level programming, in contrast to web development, is a (justifiably) conservative field with regard to choice of tools. For example, "I write ANSI C because ANSI C is the standard" is an attitude I frequently encounter. ("I write ANSI C because everything has a compiler for ANSI C and it never changes" is probably what a lot of them are getting at.) Things like breaking changes, however minor, and "just use nightly" are anathema to this crowd. Yet this is the domain that could arguably benefit from Rust the most. I think Rust needs a strong foothold somewhere to prove its maturity before it can attack the C/C++ "heartland".
>What makes you think that the languages which Rust displaces aren't also niche?
Any definition of "niche" that includes C or C++ is meaningless.
Eh, depends on where you work, in gamedev land we loved to play fast & loose with nightly/etc(within reason). Heck, I'd argue that crowd is even wilder than the JS ecosystem, it's just not as public.
Really, you might want to check your echo chamber a bit. Native programming is not the norm in the industry, most fresh grads have touched C or C++ once or twice and know the theory but none of the practice. Heck back when I was in college we had people coming to our community college to take the C course there since UCSD didn't offer it as part of their curriculum.
Now, does the majority of software run on C/C++ based systems? Totally.
However I would posit that the number of people who build those systems is much smaller than the number of people working in Java/Javascript/Python/C#/PHP/Ruby/etc. Your LoB app doesn't need the performance of C++, you just use a DB that's built with C++. You may use ngnix but the webserver behind it is probably written in Java.
There's an inverted pyramid in software. The lower down the stack you go the more specialized and domain specific you get. Component/app/framework reuse means that you need less people at the bottom then you do at the top otherwise we'll all be fullstack web/frontend/backend/driver/kernel/vhdl developers.
Either way I think Rust has a rich and vibrant community which isn't going away anytime soon. Would it be nicer to see wider adoption? Sure, but I'm not worried about it either.
The really awesome thing with rust is how easy it is to make library code which can be called from any language including C and C++ (in most situations) - just as easily as writing a library in C or C++. In some situations even easier than C++.
Thus I can easily see rust replacing C/C++ as the default language for writing 'high performance libraries' in, for use in Ruby/Python/etc. It's usually more similar to what higher level programmers are used to too. You get to use functional code for a start.
But also exactly as in Firefox - libraries / modules can be written in Rust, and then brought in to replace existing C++ code. And I'm sure the ergonomics of this process will improve too.
If a C++ project lead / manager can say, in all honesty:
"The x component needs to be re-written for whatever reason - either major refactoring for a desired feature, or performance, or to split out to use in another product. We can either do it in C++, or Rust, and Rust will garentee no new segfaults, we can trivially parellelise a lot of it for improved performance, etc. etc. with no major disadvantages..." then Rust will inevitably grow.
There's another thing I've noticed with Rust. I get a lot of some code benefits that I've seen from functional languages(understanding inputs/outputs, preventing mutation) from Rust's ownership model.
If you want full function? Just don't pass/use anything that's mut.
Need to break that contract for performance? You still have single-ownership which gives you 90% of the above but with no performance penalty.
You still get logic errors/etc but it's a great no-compromise solution when you can afford the time to get your ownership right.
> If you want full function? Just don't pass/use anything that's mut.
Not quite. There are still mutable globals (they just have to have to have the appropriate "I'm MT-safe" marker traits); and there's nothing preventing any function from performing any I/O that it desires. Even better, once specialization lands, generic trait-functions will be able to behave differently when called on different types, even if the special behavior isn't valid given only the public type-signature's assumptions.
WebRender is replacing the most core part of the browser. They are replacing the hardest part, not the stright-line simple code. I suspect that in Firefox, like in many projects, the most modules are relatively peripheral but represent a majority of the LoC.
> If Rust doesn't find its "killer app" I don't see it rapidly growing like Go (network services, containers) or Swift (everything Apple).
I don't believe that Go or Swift are growing because of their technical merits. Swift is essentially forced by Apple upon any developer who needs to develop applications that run on Apple products, and Go, in spite of its pedigree, can't be sold to newcomers without waving the Google brand.
> Widely displacing C is a pipe dream.
For old projects, sure. Yet, for greenfield projects then, given the choice, Rust does offer quite a lot of sought-after features that C is sorely lacking.
>I don't believe that Go or Swift are growing because of their technical merits. Swift is essentially forced by Apple upon any developer who needs to develop applications that run on Apple products
It's also a very good language, in par with Rust, and with the creator of LLVM behind it, and the creator of Rust (and many other Rust people) working at Apple in Swift.
>Go, in spite of its pedigree, can't be sold to newcomers without waving the Google brand.
And yet, Dart never got anywhere, despite the "Google brand" (and far more support initially, including official branding, an IDE, and having their #1 compiler guy working on it).
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.
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.
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:
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
For Haskell, the best I've heard is Facebook for some custom dev tools and Standard Chartered. I'm sure there's more, but...
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.
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.
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.
Regarding the OP, I'll quote a comment from reddit: 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."