ATS certainly looks interestinb, but it's an academic language (of which there are many) that most people probably haven't heard of... At some point, the momentum of a new programming language is just as important -- in practical terms -- as its formal attributes and qualities.
Popularity and momentum translate into (and are proxies for) important things like: library availability, long-term maintenance and support, more edge cases are explored (so less “research”, breaking new ground and bugs when going off the beaten track), tooling and even availability of teaching material like documentation and tutorials.
In case of ATS, any C library can be treated as a "unsafe-marked" ATS library, so there's no problem with library support, the problem is with their formal verification. And Rust libraries regularly suffer from the same lack of formally-verified and proven-to-be-safe APIs.
That helps with the "library availability" sub-point specifically, yes. However, there's a more than that when evaluating a language, as suggested by my comment above.
In any case, if one is discussing modern and safe languages, there's a dramatic difference between using a C library and using a library native to the language. Even ignoring safety, the ergonomics/developer experience is dramatically different and the impedance mismatch can be very frustrating (for a "best case" example of this, Swift puts a lot of effort into exposing Objective-C interfaces as "swiftier" APIs automatically, but this benefits significantly from a relatively opinionated set of idioms in the source language, something arbitrary C libraries do not have).
You're right that being able to import a C library directly is a very nice feature.
> And Rust libraries regularly suffer from the same lack of formally-verified and proven-to-be-safe APIs.
Right... but having a larger community means there's a much higher chance of a safe or easier-to-use library existing for any particular task. In particular, I think it means there's almost certainly more libraries in total, with more safe libraries and more unsafe libraries overall, so simply comparing number (or proportion) of low-safety libraries is misleading.
(Formally verified is shifting the goal posts here: the bar is just "has a native library".)
> (Formally verified is shifting the goal posts here: the bar is just "has a native library".)
It is, but it is for a good reason - ATS formally verifies your safe functions, so you only need to implement your proof once and make a compiler agree with you, and then you can save on a community-driven code-review process. Rust, on the other hand, provides safety guarantees only for a subset of safe guarantees that ATS provides. Pointer manipulations have to reside in "unsafe" blocks, and that leads to CVEs - https://gts3.org/2019/cve-2018-1000657.html
It's moving the goal posts and changing the point of the discussion. We can equally well say that that "Rust formally verifies your safe functions", and that this reduces how much code review is required... it's a matter of degree and specifics.
Focusing on pointer manipulations is also misleading: it's entirely true that it's dangerous, but most Rust code does not need to do any sort of raw pointer manipulation. For instance, there's extensive work on operating systems and other low level code that involves both inherent unsafety due to hardware specifics (that is, ATS almost certainly does not model it natively) and safe Rust wrappers (i.e. proofs of safety) for the unsafety at a surprisingly low level:
> We can equally well say that that "Rust formally verifies your safe functions", and that this reduces how much code review is required... it's a matter of degree and specifics.
You cannot say that while this kind of CVE is possible https://gts3.org/2019/cve-2018-1000657.html and as long as Rust is not capable of performing safe pointer manipulations. The above issue may be solved for VecDeque in stdlib, but what about other data structures and algorithms in the wild?
> Focusing on pointer manipulations is also misleading
Remember that the discussion is happening in the topic about brining Rust into well-established C codebase, and C uses pointer-based arithmetics all the time, sometimes the whole algorithms are implemented this way because it brings efficiency to lower-level interfaces that are supposed to be very fast. If the motivation to bring a new tool is pronounced as "let's make it safe", why should we allow the argument to fallback into the "unsafe Rust" territory?
> For instance, there's extensive work on operating systems and other low level code that involves both inherent unsafety due to hardware specifics
I'm not going argue against that, because it's not related to the current topic related to Linux Kernel.
it's not more, it's one specific example. Shall we now enumerate all the things that both languages are able to prove? I think we should, to make it clear what the differences are and what is possible to prove safe. That's exactly my point about comparing brining Rust into existing C codebases with alternative tooling available specifically for C codebases.
"In the wild" one hardly ever has to write unsafe Rust data structures and algorithms.
> If the motivation to bring a new tool is pronounced as "let's make it safe", why should we allow the argument to fallback into the "unsafe Rust" territory?
Because going from 0% of code proven safe by the compiler to 99% is very valuable. Verifying the remaining code is desirable but not as valuable as what Rust already provides.
Having said that, it would indeed be great to have a proof system for verifying properties of unsafe Rust code. Much work has been done in that area: https://alastairreid.github.io/rust-verification-tools/ Something to look forward to.
> "In the wild" one hardly ever has to write unsafe Rust data structures and algorithms.
one has to do it all the time if cyclic mutable graphs or specific buffers/caches are involved.
> Verifying the remaining code is desirable but not as valuable as what Rust already provides.
How do we know that? What are the criteria and the thresholds that lead us to that conclusion? Is it true for all fields where the language can be used? What should we do about inability to express more precise constraints at compile time? Shall we stop on Rust, or try to embrace more powerful tools that already support Dependent Types in low-level systems programming? These checks enable a whole new world of expressive powers and correctness guarantees, even compared to the cool borrow-checker. ATS supports them today [1]
"Specific buffers/caches" is ambiguous. For embedded systems there are crates that provide safe interfaces to memory-mapped hardware.
You will likely argue that using unsafe code in a library is just as bad as writing unsafe code, even if that library is used and tested by a lot of people and the unsafety is corralled behind a safe API. You would be wrong.
> How do we know that? What are the criteria and the thresholds that lead us to that conclusion?
My current project is 170K lines of Rust code, and has 225 uses of unsafe. That's about 1.3 uses of 'unsafe' per 1000 lines of code. If I could write C++ code and introduce less than 2 exploitable vulnerabilities per 1000 lines of code I'd have an even higher opinion of myself than I already do.
> Is it true for all fields where the language can be used?
I'm sure we're both imaginative enough to dream up some "field" narrow enough to disprove any universally quantified proposition.
> What should we do about inability to express more precise constraints at compile time?
We should adopt proof systems that let us verify safety properties for those little bits of unsafe Rust code. We should not, however, make that a precondition for writing that vast majority of code that can be written in safe Rust in safe Rust.
> Shall we stop on Rust, or try to embrace more powerful tools that already support Dependent Types in low-level systems programming?
That is a false dichotomy.
Safe Rust is a sweet spot where the compiler and tools can verify a strong set of safety properties without the developer having to deal with proof systems and dependent types, with lots of engineering to produce helpful messages when things go wrong. Plus a large library ecosystem that, among other things, provides lots of safe abstractions over unsafe code. Trying to put the brakes on Rust and get everyone to buy into ATS instead is putting the needs of the few over the needs of the many.
> I can have cyclic graphs with mutable data without writing any unsafe code
You can, because the libraries that you use fallback to unsafe blocks. How about those who want to write these libraries without having to use unsafe?
> You will likely argue that using unsafe code in a library is just as bad as writing unsafe code, even if that library is used and tested by a lot of people and the unsafety is corralled behind a safe API. You would be wrong.
just because you think I'd be wrong doesn't prove me being wrong. Why should I rely on unsafe if I can implement the same algorithms and data structures with proper safety guarantees, but not in Rust? Why should I stick to Rust specifically for that matter?
> My current project is 170K lines of Rust code, and has 225 uses of unsafe. That's about 1.3 uses of 'unsafe' per 1000 lines of code. If I could write C++ code and introduce less than 2 exploitable vulnerabilities per 1000 lines of code I'd have an even higher opinion of myself than I already do.
yeah, it shows your personal commitment to Rust toolchain. This is good. But what if you've already acquired some knowledge of more powerful tooling out there, and you're given a task to estimate applicability of these two toolchains to the development of Linux Kernel?
> We should adopt proof systems that let us verify safety properties for those little bits of unsafe Rust code. We should not, however, make that a precondition for writing that vast majority of code that can be written in safe Rust in safe Rust.
Why shouldn't we do it specifically for Linux Kernel? Why shouldn't we use compile-time checks for element incusion, length-based non-emptiness of containers instead of implementing another set of runtime validators?
> Safe Rust is a sweet spot where the compiler and tools can verify a strong set of safety properties without the developer having to deal with proof systems and dependent types
How do you define a sweet spot? Is it indeed a sweet spot when it comes to kernel development? Why does this spot happen to be at the level of Rust type system, and not somewhere else?
> Trying to put the brakes on Rust and get everyone to buy into ATS instead is putting the needs of the few over the needs of the many.
I'm actually arguing here from a position of technical merit of two tools in the context of Linux Kernel development, but for some reason you bring vague and non-technical definitions of "sweet spot", "lots of people using something", "needs of the few vs needs of many", which I've not mentioned anywhere in the thread.
> In any case, if one is discussing modern and safe languages, there's a dramatic difference between using a C library and using a library native to the language.
The dramatic nature of that difference is whether that library exists or not. Odds are, if exists then it's written in C. Thus this point is mute with regards to Rust because at best it's relegated to a nice-to-have, in the sense you can enjoy the same features that are already available in C but with language-specific assertions.
Ah, furthermore, looking at a comment below, it seems ATS's support for C libraries is almost identical to Rust's: specify a list of functions and their signatures on the ATS/Rust side. From your adoring descriptions, I had been assuming it simplified the process properly, by allowing importing a C header directly (like Swift can).
(The main difference seems to be ATS allows inline C, since it looks to be tied to C as a compilation target.)
Choosing an obscure language with little community support imposes real-world development costs: it's harder to find or ramp up new developers, there are fewer eyes identifying bugs in the implementation, tooling support can be subpar, documentation and blog posts are harder to find, etc.
(btw I know nothing about ATS so I'm not saying this is a good description of that language in particular.)
I agree with your points regarding tooling and dev support in general. ATS, in that regard, benefits from being a "frontend compiler" to GCC - all the tooling for GCC can be used equally well for ATS codebases. Developers need to know C well (not an issue with all the learning material available), and at least one language from ML family (OCaml, Standard ML, F#, Haskell to some extent) to quickly pick up the syntax and common recursive constructs. There are three great books [1] available online, and a collection of common system programming examples that demonstrate how data types and algorithms can leverage safe language features [2]
Popularity is not quite the same as PR. But yes, it's about the number of engineers and projects using it, and the growth of such adoption. If technical merits were the only criteria for making a difference, I think it's fair to say we would have a very different technology ecosystem today. :)
Yes, it really does if you're talking about success. Just like with Betamax vs VHS, and many, many other examples over the years. Technical merit is only one small part of a success story, and it's not the most important one.
