“I hope to see a switch from C to VB very soon. I've already spoken with various luminaries in the C coding world and most are eager to begin to transition. Having just gotten off the phone with Mr. Alan Cox, I can say that he is quite thrilled with the speed increases that will occur when the Linux kernel is completely rewritten in Visual Basic. Richard Stallman plans to support this, and hopes that the great Swede himself, Linux Torvaldis, won't object to renaming Linux to VB/Linux. Although not a C coder himself, I'm told that Slashdot's very own Admiral Taco will support this on his web site. Finally, Dennis Ritchie is excited about the switch!”
At very least the Azure Sphere OS team should finally adopt Rust, instead of doing security marketing with the 7 layers of whatever, and then shipping a C only SDK.
It is like they are absent of the company security efforts, while trying to sell us a story of how much they care about security.
If I remember well, only 512KB is actually usable by OEM applications on that platform.
I was using C++ on MS-DOS.
Not even C++ is supported on the Azure Sphere OS SDK.
Ironically they usally tend to evade the question when asked about it, to the point they ended up writing a very long blog post trying to justify C, and it had nothing to do with space requirements.
Rather industry expectations and other marketing speak.
So instead of including a custom runtime they just bailed out...
Anyway just search for Jason Turner's talks on targeting Commodore 64 with C++.
No. They are only using C. They are not using anything else for "unknown" reasons.
You can write bloated Rust applications in pretty much the exact same ways you can write bloated C applications (generics, runtimes, macros, ...).
And you can write thin Rust applications in pretty much the same ways you can do so in any other language, including C.
Ada may be a good language, and GNAT may be a fine Free and Open Source Ada compiler, but Ada isn't a new programming language. Software developers only chase shiny new things. Ada is held back by its beginnings as a niche language with expensive compilers, it doesn't matter that this hasn't been the case for decades now.
I think one big stumbling block people had in adopting ADA (along with there not being a good open source toolchain for a long while as noted here) is that it just looks different to people that primarily use C and similar languages, and that puts some people off.
That's sad, and I would rather it not be true, but it's become increasingly obvious to me from how people treat numerous newer languages I've seen pop up over the years.
I'd be more than willing to give Ada a chance, but when I looked at code samples I definitely had to fight an automatic response of thinking it was something out of date based on how it looks.
It's not that there aren't successful languages and have a different look and feel, it's that there's pushback against them when they are targeted towards the niches C and C++ are already strong in. Obviously many languages exist and many have become popular, but certain niches are more resistant than others and sometimes it's for non-rational reasons.
> I'd be more than willing to give Ada a chance, but when I looked at code samples I definitely had to fight an automatic response of thinking it was something out of date based on how it looks.
That's part, but not all, of what I'm talking about. The style C follows is damn old itself, sometimes predating the languages you're thinking of as out of date.
Maybe also, but not only. In contrast to Rust, Ada docs have been awful, and as long as you didn't get a commercial toolchain you had to play with some gimped version (and the really free version didn't come out until the language was 20+ years old), the build system was as “good” as C, people complain that Rust is verbose, but Ada was still a notch over, the memory model of Ada is a mere reflect of Rust's one, and (maybe I'm being subjective here) Rust's stdlib and philosophy is leagues over Ada's (Option, Iterator, closures, Result, ...).
Ada had the potential to be a Rust 30 years before, but it was never the goal of its owners.
That kind of thing happens; we're in a profession that is made up out of people.
Rust has opt-in memory safety issues but outside of those, does not require a GC.
Rust does not have Ada's constraint system. In that way, rust is easier (and arguably less safe) to program.
Ada didn't get the same love as Rust for the same reason D goes pretty unloved. The problem systems engineers needed solved was memory safety without a GC. Neither D nor Ada solve that problem.
Static memory allocation is totally fine if the thing you're building is, like, a control system for a jumbo jet. You know exactly how many engines you have, how many wings you have, how many pilots you have, etc. Your autopilot has a fixed set of parameters: heading, speed, altitude, etc. You know exactly what tasks you're running: watch engine performance, watch the altimeter, watch cabin pressure, find the instrument landing system and line up with it, etc. If you have some new instrument to plug in, you get a new version of the flight control software, and you're certainly not plugging in new things mid-flight. Even if you aren't running all the tasks at once - e.g., you're usually not landing the plane - you want to guarantee you could turn on any of those tasks. You never want the possibility of running out of memory when you try to land, so you want to allocate memory for landing the plane at design time that's always reserved for landing the plane, and nobody would call that a "memory leak."
A general-purpose OS like Linux is different. You can create as many processes as you want. You can mount as many filesystems as you want, of various formats, whenever you want. You can plug in devices while the system is running. You can add drivers to a running kernel and remove them too. You can configure network connections, turn swap on and off, etc. Inbound network connections can show up at any time. So it needs dynamic allocation.
Ada is fantastic for problems like a flight computer. But it's a different sort of problem. For a general-purpose OS, you are allocating and freeing things in response to user input, and you want to make sure you neither leak memory nor use memory after it's been freed.
Rust is very good at solving that specific problem without the need for a GC. That's what people mean when they say "Rust doesn't use a GC."
AFAIK short of SPARK:
* Ada has pointer arithmetic, you can overflow buffers or read out of bounds.
* Dynamic allocation is straight unsafe and unchecked (unless you have a GC, in which case… you have a GC), you can use-after-free and double-free if you copy pointers beforehand.
* Accessing uninitialised variables is not forbidden.
* You can dereference null pointers (though it should cause an exception so I guess that's memory-safe).
Not true. Arrays have bounds and those are checked. However, you can do arithmetic with the type ptrdiff_t of the package Interfaces.C.Pointers. You can also do an Ada.Unchecked_Conversion on a pointer that you get from a C function. Obviously that's unsafe.
> * Dynamic allocation is straight unsafe and unchecked
If allocation on the heap fails, it will raise a Storage_Error, but you can catch it. Also, the language has a lot of restrictions on when you may copy and store a pointer.
> * Accessing uninitialised variables is not forbidden.
True, but there are pragmas like Normalize_Scalars (to initialize them to invalid values) or Initialize_Scalars.
> * You can dereference null pointers
True, but dereferencing will raise an exception. Also you can define non-null pointers like this:
type Foo_Ptr is not null access Foo;
procedure Bar (Value : not null Foo_Access);I don't have enough experience with Ada to comment on whether its verbose and keyword-heavy syntax succeeds in this goal.
For me, its always the var/function names and comments that determine how readable a program is.
So that's like... your opinion, man.
SQL is another 'wordy' language. There are many, many things wrong with the SQL language, but I wouldn't say its wordiness is one of them.
It's not like Microsoft isn't pushing Rust on their own platform. Every time a Windows driver does a use-after-free somebody swears at Microsoft for causing a bluescreen.
I've never read anything to make me think that Rust is a safer alternative than any of these options; the guarantees of the language are just assurances of its advocates.
[0]: https://www.fstar-lang.org
[1]: https://www.microsoft.com/en-us/research/project/checked-c/
[2]: https://www.microsoft.com/en-us/research/project/vcc-a-verif...
[3]: https://github.com/koka-lang/koka
[4]: https://github.com/dafny-lang/dafny
[5]: https://www.microsoft.com/en-us/research/project/project-ver...
I know Rust; I don't know Frama-C or Idris or Ada. What little I know of Ada indicates that it doesn't actually solve the problem because it doesn't have safe dynamic memory allocation. Ada advocates have told me I'm wrong and there's some new thing (inspired by Rust) that does this. Maybe! I'm not sure there's any benefit to the world in arguing it; someone skilled in Ada should just write something and show how it would actually work.
Write a kernel module with any of those techniques, send in a patch, and see what people say. Any effective means of making the kernel less buggy is great. It doesn't have to be Rust.
I claim that Rust is effective because, well, those patches are there, and frankly I haven't been doing any work for this project in almost a year and we're getting so many enthusiastic contributors. So, apparently, a lot of other people also know or are willing to learn Rust. Maybe it's actually better than the alternatives you mention; maybe it just has better documentation. I don't know. I'm not claiming Rust is perfect, just that it's empirically likely to solve the problem.
If you can get together a community of folks who can do any of these other approaches, that would be fantastic. Try it!
It does, just not the way most are used to it.
Surely if one wants to code like malloc()/free(), free() is unsafe in Ada and requires the Ada version of unsafe {}
However many type constructions in Ada do dynamic allocation by themselves, including on the stack.
If memory allocation fails, an exception is thrown and a retry with less memory requirements is a possible execution path.
Ada also has RAII since Ada95 (controlled types), and yes SPARK formal specification now allows for ownership rules.
So, since we're talking about the Linux kernel, that's a red flag straight away. Notice a whole section of this new LKML post is about their implementation of Rust's alloc crate? Linus doesn't want useless exceptions here and has previously objected on that basis.
Meanwhile... Over in the C++ world they have this same behaviour. For them these exception handlers are a fiction, in reality popular standard libraries (never mind everything else you're using) will blow up in low memory and it's game over. Maybe Ada does a lot better. Maybe.
Ada also has no exception allowed profiles and other mechanisms.
HN is not the place to hold a lecture on Ada features.
It is not a maybe, rather lack of knowledge.
We can lead academic discussions about which language is safer/better/leaner/whatever-er, but the fact is that Rust has a larger and growing mindshare so this effort is unsurprising. For Ada, the solution isn't to try and prove to anonymous forum goers it would've been better choice if only people recognized the fact. The solution is to mobilize the Ada community to put the same amount of effort into the publicity and marketing (yes, the bad M word) of their ecosystem.
Ada clearly lives on in many safety critical systems, but judging by the admittedly biased topic frequency on HN and other technical sites, it has a tiny community who mostly keep to themselves. That's fine, but then don't be surprised when it's Hip Language X that gets the headlines and these sort of efforts.
My only point is how many in the Rust community advocate as if Rust would be the first language having features, that actually were already in Ada for the past decades.
As for Ada on Linux, naturally Linus would never go along it.
A C kernel guy liking a language with Pascal syntax, a community that worships a paper that hasn't been true in the Pascal world since early 80's, not even at gunpoint.
If you want to see a use case where Ada was chosen against Rust, check NVidia's project for self driving vehicles firmware.
Plenty of safety conscious language have had followings since ALGOL, this is the point that many miss when praising Rust, while ignoring our computing history.
I think that is a false perception created by the dev-blogging community. Based on GitHub activity (https://madnight.github.io/githut/#/pull_requests/2021/2) Rust usage is declining (absolute numbers show little growth). Based on developer surveys (https://www.jetbrains.com/lp/devecosystem-2020/) very few people use rust outside of hobby development.
I think the concern is that the core argument that "I think Linux should adopt rust for safety" is a bit dishonest, given that there are a large number of well-vetted alternatives. "I think Linux should adopt rust because I like rust for social reasons" would probably be more correct. That Google staff seem to think rust is good for the Linux kernel but not, say, Zircon, would be surprising if those same people actually believed that any legal rust program is safe and inherently trustworthy. "Embrace, extend, extinguish" wasn't that long ago.
I mean, neither Ada nor Zircon are even on the lists, so in terms of mindshare, they are clearly blown out of the water by Rust (from the evidence you provide). To discount Rust based on usage when the alternatives being suggested don't even make the rankings is also a bit dishonest.
In fact, the argument "I think Linux should adopt rust for safety" makes perfect sense. Here's finally a safety conscious language that seems to be embraced by a larger community, and even the big tech players. Instead we get people suggesting arcane alternatives that may be technically better, but have a snowball's chance in hell to become commonplace any time soon.
In the meantime, Google makes extensive use of Rust in new components of both Fuchsia and Android and even rewrites some legacy components where it makes sense.
I think you and 'grumblenum should team up and write a working kernel module in Ada/Spark and then we can have a fruitful discussion about it, instead of just theorizing about whether it could be done. I'm interested in seeing the problems solved, and I'm indifferent to technology. If you think Ada/Spark can solve them, that would be awesome!
(Editing to reply to a small claim in another subthread, "Linus would never go for it" - we believed the same thing when we started. We were originally thinking that we'd pitch this directly at Linux distros shipping out-of-tree modules that they didn't want to keep having to push security updates for. https://github.com/fishinabarrel/linux-kernel-module-rust was out-of-tree and we tried to keep compatibility with kernels 4.4 onwards. But it turned out Linus isn't opposed to it.)
https://www.adacore.com/academia/projects/muen-project
https://www.adacore.com/company/partners/nvidia
https://genode.org/about/road-map
https://www.ptc.com/-/media/Files/PDFs/Developer-Tools/apexa... (ApexAda Exec)
https://www.ghs.com/products/safety_critical/integrity_178_e...
https://www.windriver.com/products/helix (Wind River Helix Bare Metal partitions)
Muen: If I am reading the allocator in https://git.codelabs.ch/?p=muen.git;a=tree;f=tools/liballoc/... correctly, it simply has no deallocator function at all. It does have a "Clear" function, but there's no sign that it has any ability to statically check that calling it is safe. That is exactly what we're talking about.
Nvidia: No public source code, and it's not obvious what actually exists here, beyond a compiler to Nvidia hardware.
Genode: This project is mostly written in C++. There is a very tiny, experimental amount of Ada in it (< 400 lines of code). There's certainly nothing that speaks to the questions discussed in this thread (safe dynamic allocation/deallocation, security, etc.).
ApexAda: This is a marketing brochure. Also this marketing brochure talks about "significant deployments in satellite communications, avionics, weapons control systems, and a myriad of other mil/aero applications," all of which - as discussed elsewhere in these comment - are applications that neither need nor want dynamic allocation (and are generally not exposed to deeply-structured untrusted input, for that matter).
Green Hills: This looks interesting - there's a POSIX filesystem and a UDP socket implementation, both of which (probably) want dynamic memory allocation. That is, at last, an application that needs dynamic allocation. Is it actually written in Ada? I see that the RTOS itself supports development in C, C++, and Ada, and they claim to offer a BSD socket implementation, so they at least have C bindings. I don't see any claim about what language it's written in, and Green Hills seems to do a lot of C work (see e.g. https://www.ghs.com/products/micro_velosity.html). If it's in Ada, then I think this gets the closest to what would be needed for the Linux kernel - do you know how their filesystem and socket implementations handle dynamic allocation? (I'll also note that they lost their certification many years ago, so if the answer is that they have safe code because they spent a whole lot of time perfecting a single version of an OS, then that's a very different problem space from Linux, which is constantly changing.)
Wind River: This is a marketing page without much detail, but it looks like it's a hypervisor to run general-purpose OSes on top of, not a general-purpose OS itself, which means it probably does not need dynamic memory allocation, or that if it does, the safety of deallocation can be verified by hand.
---
No Ada developer has done what's being done in this patchset, and it's pretty insulting to the folks putting in the work to claim it's been done and Gish-gallop a bunch of random links and expect people to put in the time to figure out what exactly you're claiming already exists. Everyone knows it's possible to write code in Ada. Nobody is asking if Ada can be used for completely unrelated purposes. You may as well link to GORILLAS.BAS and ask why the Linux kernel isn't using QBasic, a memory-safe language if you use the subset without PEEK and POKE.
Write - or point to - a kernel driver for a UNIX-like operating system written in Ada, that safely handles dynamic allocation. That's the clear bright-line goal. If you think that's not the right goal, say why.
I think the first problem is some kind of language specification. That it's not possible to know what behavior one should expect from rustc means that it isn't a solution. It's another problem. You should check out Ken Thompson's great speech on why this is an issue. https://www.cs.cmu.edu/~rdriley/487/papers/Thompson_1984_Ref...
Or do you think it's wrong to regard unauditable enhancements to free software paid for by Google with suspicion?
Here's a way to address the issue he brings up in that speech that does not involve language specifications: https://dwheeler.com/trusting-trust/
>just that it's empirically likely to solve the problem.
Can you comment on what empirical evidence you based this statement on?
Yes, I can comment on this. The licensing is the same as any other submission to the Linux kernel. See https://www.kernel.org/doc/html/latest/process/license-rules... for Linux kernel licensing in general and also https://www.kernel.org/doc/html/latest/process/submitting-pa... for the meaning of the Signed-off-by lines.
> Can you also comment on how a third party can verify or audit the output of a compiler without a specification?
I imagine it's pretty similar to how you verify or audit the output of a compiler with a specification. If you can show me an example of the sort of verification or audit you envision, I can perhaps give you a more helpful comment.
We do not make any claims about verified or audited compiler outputs or compliance with specifications, and to the best of my knowledge, the Linux kernel does not currently verify or audit any compiler outputs, so I'm not sure I follow why I would be particularly qualified to comment on it, but I could maybe point you at some interesting research.
> Can you comment on what empirical evidence you based this statement on?
Yes, I did comment on this, in the paragraph you quoted. If you'd like me to expand on something can you clarify?
I must be missing the humor here. You can test against a specification to verify implementation. Testing an implementation against itself is meaningless. I would think that this is obvious. Also I don't typically use the word "empirical" to indicate purely qualitative assessments or intuition. You also provided a dead link.
There's no attempt at humor here - I'm just trying to get you to explain what, precisely, you mean by "test against a specification to verify implementation" so that we're in agreement on terms.
When I hear "test against a specification" and "verify implementation," I think about things like CompCert. But the Linux kernel does not use CompCert, it uses GCC or Clang. To the best of my knowledge, neither is tested against a specification and neither has a verified implementation.
Actually, when we first started discussing mainlining this, we had a bit of discussion about whether it was safe to allow rustc-compiled Rust code to link against GCC-compled C code. The specific worry was potential compiler bugs, of which the kernel has historically run into many. We eventually decided the risk was low, but the kernel has gone through periods where it insisted you use the exact same compiler for the kernel and for modules because of bugs. Those bugs have gone away through the normal human process of writing better code, not through formal verification. And when they existed, the kernel's response was not to reject those compilers, it was to work around the bugs.
Also, CompCert does not test against the C standard, which is written in English prose. It tests against the CompCert developers' attempt to re-express the C standard in terms of machine-checkable theorems. The C standard is confusing even to human readers, so it would be misleading to say that CompCert has verified their compiler against the standard as published by the standards committee. (Hence my claim that they're similar; you can verify a compiler of any language provided you write your own machine-checkable statements about what you expect it to do, and you still need other humans to read those theorems and convince themselves that they're the right ones.)
For those reasons, I'm trying to understand what your question is in a precise manner. Are you asking about things like CompCert? Because if so, I don't follow the relevance to our work, though again, I'm happy to point you at interesting research.
But Rust has a lot more going for it than safety. Maybe it shouldn't matter for kernel code, but the focus on developer "ergonomics," high-level functional constructs and pretty flexible pattern matching, supporting both ML-style and Algol-style syntax, very strong language-level tooling for building, testing, packaging, and generating documentation, plus the fact that the language itself is so well documented with great, accessible tutorials.
There's a reason it keeps winning Stack Overflow's most loved language award every year. It's easy to learn for people coming from almost any kind of programming background, supportive of newbs, and equally well-suited for application-level and system-level development, so it ends up with pretty widespread appeal.
So again, I don't know that any of this should matter for selecting what languages you're going to support in the kernel, but as a purely practical matter, it's a lot easier to ask contributors to use a language they already know and use elsewhere than it is to ask them to learn something new that they don't use anywhere else, which is what Ada and Idris and what not would be for most developers.
FWIW I would trust anything language-level over applying static analysis tools to C (for an evolving codebase like Linux, having the safety be a first-class part of the codebase is a must) or extracting C from another language (the semantics of C are surprisingly weak, such an extraction can only ever be as good as your model of C which will probably be buggy).
What Rust focuses on is providing a scalable approach to a limited kind of formal verification - focusing purely on type- and memory-safety, not conformance to arbitrary specifications. The latter is of course being worked on, but type safety and memory safety are table stakes.
For instance, I have to deal with JSON. There's no reason older languages can't deal with JSON, but it'll often be inconvenient as the libraries try to deal with mismatches in the type system or whatever, and it just can't ever be quite as slick as a more modern language written with some partial, vague combination of the fact that JSON exists in mind, together with the sorts of techniques used to implement JSON support in modern languages. Or sometimes it'll just be the dominant library for dealing with it just has an old design that baked bad assumptions in, and since it's the dominant library it's the one everything uses, so I have to deal with that everywhere.
And it's just the death of a thousand of those cuts. "But you can do JSON in my favored language!" Yeah, but it's just not quite as slick. "But we have an HTTP client in this language!" Yeah, but it's just not quite as slick. "But we have GPU support in my favorite language!" Yeah, but it's just not quite as slick. And you've ground all that "not quite as slick" deeply into your language over the decades.
So nobody has any one reason they can point at as to why Ada isn't going come back, or why E isn't going to come back, or why Cyclone isn't going to come back... but the reality is that the sum total of the issues is more than sufficient to prevent it from ever happening, and what's going to happen is a more modern language is going to get the support.
Advocates also try to "defeat in detail", in analogy to the military technique, arguments to the contrary, but the problem is that while that may satisfy the advocate, everyone else is still left looking at a metaphorical battlefield that has an exhausting number of "battles" over basic deficiencies, and being "defeated in detail" by an advocate just transfers to exhaustion with the underlying language anyhow.
It probably isn't a "the issue" with Ada/SPARK. It's a horde of small little things, the sum total of which is too much hassle for anyone to want to deal with.
I’m also not sure why “nice JSON libraries” is a hard requirement for kernel code. Also, see JWX.
What does happen with such languages is that someone comes along and creates some sort of new language taking the best of the old language and mixing it with more modern stuff. I personally think there's an Ada-like niche waiting to be exploited there, probably something that also takes some lessons from Haskell. (Haskell is still alive, but IMHO, headed toward this sort of dead right now, and really could use this sort of revival itself.) An example of this is Elixir... Erlang would probably be also something I'd be calling "dead" if it weren't for Elixir.
(Ironically, often the biggest partisans of the base language are the last to know about the revival language because every deviation from the base language is seen as a flaw from the One True Answer....)
> That never happens. It may well klunk along for more decades... but it's dead
Ada is used in 2021 in the exact same places that Ada was used in 2011 (and 2001 before it), if not more. Ada was designed for a specific purpose, one that it still fulfills very well. People have been claiming Ada was dead for decades, yet still it miraculously lives on. Despite Rust, despite Haskell, despite an algal bloom of "formally verifiable subsets of C", and so on.
> What does happen with such languages is that someone comes along and...
Yet... This just... hasn't happened. A successor language more suitable for safety-critical development has just simply not appeared. The manufacturers using Ada —a subset of which can be seen at this[3] link— ostensibly don't seem convinced that any of Ada's many alternatives offer a more appropriate solution for developing safety-critical software.
> I personally think there's an Ada-like niche waiting to be exploited...
The Ada-like niche you describe is, believe it or not, currently occupied by Ada. Ridiculous as this may sound, Ada is actually pretty good at fulfilling its intended function. What needs to change? Ada is not designed to fill the role of Node.js, Java, or C#. It's designed for safety-critical embedded systems, which is where you're most likely to find it today.
> Ironically, often the biggest partisans of the base language are the last to know about the revival language because every deviation from the base language is seen as a flaw from the One True Answer...
Does this apply to your thinking too, or just the proponents of Ada, and other languages you don't like? Are the Rust users just blind to the benefits of Ada? Are you susceptible to the same cognitive blind-spot you accuse us of having?
[1] https://www.npmjs.com/package/pad-left
Wait! There is Alire[1][2]! There is a list of "crates", you can easily include them into your project, and so forth. This is pretty much the same as https://crates.io or https://pkg.go.dev, which means people really should throw their misconceptions away and actually do some research before concluding that the language (Ada) is dead. A couple of quick searches quickly tells me that Ada is pretty much alive, with all of these "modern libraries with modern solutions", and full-on safety without performance loss.
This comment is intended for the person you replied to. :)
[2] https://blog.adacore.com/first-beta-release-of-alire-the-pac...
Too long of this pattern and it becomes much more trouble than it's worth to use on a business level.
They gave a bunch of reasons.
Now, I know that there is a trendy view of "the more the better", and it does not have as many libraries there, but that has to do with the fact that it is not yet widespread among Ada users. Alire is really new.
What are types if not arbitrary specifications? Are you suggesting that formally verified software is not memory safe? What on earth does "scalable" even mean? A verified program cannot scale? If not, why not?
I believe the comment that types are aligned with the syntax is meant as a contrast to other languages which include specifications written in a format substantially different from or fully removed from the implementation. This can reduce the friction of using type-based verification when compared to formal verification capable of describing an arbitrarily complicated spec.
When discussing the scalability of types, I think he is saying that because types are coupled to the implementation, and don't support non-local reasoning, it is less likely that you will run into issues with type checking as you try to compose many small components into a larger program. In contrast, my impression is that with full formal verification, it can become extremely difficult to properly verify a large system.
Regarding your comparison to C and python, I think it's clear that the parent was comparing the specific type system and borrow checker that Rust provides vs. formal verification, not making a statement about the general concept of a type system. In particular, I don't think it's reasonable to assume he was saying the existence of types provides any sort of safety. Rather, it's clear he was saying the use of a powerful type system (such as that found in Rust or Haskell) to implement a limited specification of the program functionality can provide a degree of safety.
"In other words, the Curry–Howard correspondence is the observation that two families of seemingly unrelated formalisms—namely, the proof systems on one hand, and the models of computation on the other—are in fact the same kind of mathematical objects.
If one abstracts on the peculiarities of either formalism, the following generalization arises: a proof is a program, and the formula it proves is the type for the program."
I'm assuming "scalable" in this case is referring to the fact that fully verifying a piece of software is currently takes a large amount of effort. Rust's approach is more "scalable" in the sense that they decided to focus primarily on memory safety, and punted on other forms of verification in the hope that it would be more ergonomic/require less effort.
Note that some formal verification work has been done on the guarantees that the borrow checked provides (which led to finding and fixing an edge case bug), so there is a little more concrete evidence that just the "assurances of its advocates"
See http://plv.mpi-sws.org/rustbelt/ for more information, also the verification working group: https://rust-lang-nursery.github.io/wg-verification/
You might want to look harder, because there is certainly a verified language subset (anything that can be written as LambdaRust, which covers a large and substantial swathe of the language).
If you're looking for a formally verified, optimizing compiler for any realistic language, particularly a low level language, you have pretty much one option: CompCert (I'm not sure where this large group of verified compilers you claim exists lives, but I'd love to see them). As someone who would love a verified Rust toolchain, I can't help but notice that very few safety-critical systems actually use CompCert in practice, which makes me a bit suspicious of claims that this is something Rust needs to be competitive in this arena.
Finally, I'll point out that verified compilers like CompCert only promise to translate correct C to correct machine code; they do not necessarily aid you in coming up with correct C in the first place. Miscompilations certainly happen, but not nearly as often as undefined behavior in the source program. So asking why people would use Rust when verified compilers exist for other languages is sort of missing the point.
Also, there is only undefined behavior in rust. The compilers behavior can change at any time for any reason any time somebody with commit rights thinks that it should. You cannot begin to assert provenance about some thing that can change at any time.
I somewhat doubt this, but even if it is true, the fact remains that people are not actually using it for the vast majority of mission-critical software. This suggests that the elimination of miscompilation bugs, which is what you get from formal verification of a compiler, is not high on their list of priorities.
> Also, there is only undefined behavior in rust. The compilers behavior can change at any time for any reason any time somebody with commit rights thinks that it should.
This is certainly not true of Rust in any practical sense.
I am not saying Rust doesn't need a certified version of its compiler that people can legally rely on for stuff like this (as opposed to practically). I am saying that this objection has nothing to do with the existence of a formally verified compiler, which is also not in practice used to compile mission-critical C programs. I think you are confusing certification of a compiler for mission-critical software, with formal verification of the language's compiler, semantics (including type safety of the safe subset--a proof that would not go through for C as it explicitly unsafe), and standard library.
(Though, as pointed out by a sibling, there is a subset that is.)
- the requirements generally change quite frequently
- the requirements are generally a long way from being "formally verifiable"
Where I, personally, have found the most value so far using FV techniques is from modelling "tricky" things whose requirements are quite solid. A few examples from my work:
- A state machine for managing LoRa communication. The requirements in the LoRa spec are pretty good. I took those requirements and designed a state machine I could implement on a low-power device and modelled that SM in TLA+ to verify that there were no deadlocks/attempted transitions to invalid states.
- A state machine for managing the Bluetooth communication between an Android app, a Bluetooth-Iridium (satellite) bridge, and the server on the other side of the Iridium link. Similar to the LoRa case, I used TLA+ to ensure that there were no deadlocks in my proposed SM (and uhh made a number of corrections as I went). Ultimately, due to the design of the BT/Iridium gateway, the exercise resulted in the conclusion that it wasn't actually possible for this process to be 100% reliable but it was possible to detect and retry the edge cases.
- Modelling a somewhat awkward email/SMS invite flow for a mobile app. You could get an invitation over email or SMS, and your account transitioned through a few different states as both your email address and your phone number were verified. Modelling this helped ensure that your account couldn't get into a state where no forward progress was possible or into a state where you could use a half-completed account.
Just a note, I (personally) don’t consider TLA+ a FV technique — it is a really good technique that actually scales much better than formal verification programs like Agda or Coq.
Is TLA+ a sandwich?
Let us see what they have, using formal verification (Ada/SPARK).
- JWX is a library for handling JSON data and more. It is implemented in the SPARK programming language and has been proven to contain no runtime errors. As a result, JWX is particularly suited for processing untrusted information.
- The RecordFlux specification language is a domain-specific language to formally specify message formats of existing real-world binary protocols. Its syntax is inspired by Ada. A detailed description of the language elements can be found in the Language Reference.
- Formally verified, bounded-stack XML library
This is just Componolit.
Let us check the F* language:
- F* (pronounced F star) is a general-purpose functional programming language with effects aimed at program verification. It puts together the automation of an SMT-backed deductive verification tool with the expressive power of a proof assistant based on dependent types. After verification, F* programs can be extracted to efficient OCaml, F#, C, WASM, or ASM code. This enables verifying the functional correctness and security of realistic applications. The main ongoing use case of F* is building a verified, drop-in replacement for the whole HTTPS stack in Project Everest. This includes verified implementations of TLS 1.2 and 1.3 and of the underlying cryptographic primitives.
---
Given the above, what exactly do you mean that it does not scale?
Features:
* AES-128, AES-192, AES-256
* AES-CBC (all supported AES modes)
* SHA-1
* HMAC-SHA1
* SHA-256, SHA-384, SHA-512
* HMAC-SHA-256, HMAC-SHA-384, HMAC-SHA-512
* PRF-HMAC-SHA-256, PRF-HMAC-SHA-384, PRF-HMAC-SHA-512
* RIPEMD-160
* HMAC-RIPEMD-160
* ECDSA, ECGDSA
It is pretty awesome. :)
For a less hypothetical example. RedoxOS has a codebase that dwarfs Sel4 (but it is still much smaller than Linux in turn), yet it type checks with much less compute cost than it takes to formally verify Sel4. Or heck, Redleaf actually formally verifies in a tiny fraction of the time it takes to formally verify Sel4, because the Rust type checker not only significantly reduces the amount of requirements that still needs to be formally verified but also reduces the complexity to verify those requirements to linear to the codebase size due to the restrictions that the Rust type system and module system puts on valid Rust programs (with a little bit of care when writing the code). Of course, until you have a certified Rust compiler there might still be miscompiles of Redleaf and until all the features of Rust used in the Linux kernel is formally specified, we cannot do the same with the Linux kernel as for Redleaf even if somehow all of Linux got rewritten in Rust. But in Rust at least it is conceivably possible given sufficient resources and sufficient time. I very much doubt it will ever be possible without help from a sufficiently expressive and practical type system.
Oh yea. Then there's another problem. Most (all?) of the examples you've mentioned have requirements that are well specified and pretty much set in stone. The requirements fro the Linux kernel... aren't quite as obliging.
It's security parameters are well-defined enough that you can use it to launch isolated VMs with... less secure OSes that are sandboxed from each other.
From a quick google, seL4 has around 10,000 lines of C code, whereas the Linux kernel has around 30,000,000.
I think CSIRO disbanding the team was a huge mistake, but in any case they weren't producing the kind of success metrics that sustained their funding.
Well [0]
https://os.mbed.com/docs/mbed-linux-os/deprecated-product/we...