原文
原始链接: https://news.ycombinator.com/item?id=41110269
该用户对使用 Rust 作为提高代码安全性和可靠性的主要语言表示担忧,理由是其编译器的大小和复杂性以及与 C 等语言相比缺乏手动可听性等问题。该用户认为传统方法,例如 使用静态分析并在 C 上构建更高级别的语言,并结合形式验证,可以提供更简单的解决方案以及更小、更易于管理的代码库。 他们指出了紧凑型 C 编译器(例如 TinyCC)和方案解释器(例如 ChibiScheme)的示例,它们允许手动验证。 最终,用户认为任何经过正式验证的系统都必须具有可手动验证的核心组件,以确保整体可信度。 总之,他们建议开发人员可能会选择接受未经彻底审核的复杂代码层,从而导致潜在风险和不可预测的结果,类似于智能家电变成有感知的实体。
- Rust's compiler is 1.8 million lines of recursively compiled code, how can you or anyone know that what was written is actually trustworthy? Also memory safety is just a very small part of being able to actually trust code.
- C compiles down to straightforward assembly, almost like a direct translation, so you can at least verify that smaller programs that you write in C actually do compile down to assembly you expect, and compose those smaller programs into larger ones.
- C has valgrind and ASAN so it's at least possible to write safe code with code coding discipline, and plenty of software has been able to do this for decades.
- A lot of (almost all) higher level programming languages are written in C, which means that those languages just need to make sure they get the compiler and GC right, and then those languages can be used for general purpose, scripting, "low level" high level code like Go or OCaml, etc.
- There are many C compilers and only one Rust compiler, and it's unclear whether it'll really be feasible to have more than one Rust compiler due to the complexity of the language. So you're putting a lot of trust into a small group of people, and even if they're the most amazing, most ethical people, surely if a lot of critical infra is based on Rust they'll get targeted in some way.
- Something being open source doesn't mean it's been fully audited. We've seen all sorts of security vulnerabilities cause a world a hurt for a lot of people that came from all open source code, and often very small libraries that could actually be much easier to audit than lines with millions of lines of code.
- Similarly, Rust does not translate to straightforward assembly, and again would seem to be impossible to do given the complexity of the language.
- There was an interesting project I came across called CompCert, which aims to have a C compiler that's formally verified (in Coq) to translate into the assembly you expect. Something like a recursively compiled CompCert C -> OCaml -> Coq -> CompCert would be an interesting undertaking, which would make OCaml and Coq themselves built on formally verified code, but I'm not sure if that'll really work and I suspect it's too complicated.
- I think Rust might be able to solve some of these problems if they have a fully formally verified thing, and the formally verified thing is itself formally verified, and the compiler was verified by that thing, and then you know that you can trust the whole thing. Still, the level of complexity and the inability to at least manually audit the core of it makes me suspect it's too complicated and would still be based on trust of some sort.
- I still think that static analysis and building higher level languages on top of C is a better approach, and working on formal verification from there, because there are really small C compilers like tinycc that are ~50k LOCs, which can be hand verified. You can compile chibi-scheme with tinycc, for example, which is also about ~50k LOCs of C, and so you get a higher level language from about 100k LOCs (tcc and chibi), which is feasible for an ordinary but motivated dev to manually audit to know that it's producing sound assembly and not something wonky or sketchy. Ideally we should be building compilers and larger systems that are formally verified, but I think the core of whatever the formally verified system is has to be hand verifiable in some way in order to be trustworthy, so that you can by induction trust whatever gets built up from that, and I think that would need to require a straightforward translation into assembly, with ideally open source ISA and hardware, and a small enough codebase to be manually audited like the tinycc and chibi-scheme example I gave.
- Worst case everyone kind of shrugs it all off and just trusts all of these layers of complexity, which can be like C -> recursively compiled higher level lang -> coffeescript-like layer on top -> framework, which is apparently a thing now, and just hope that all of these layers of millions of lines of code of complexity don't explode in some weird way, intentionally or unintentionally.
- Best case of the worst case is that all of our appliances are now "smart" appliances, and then one day they just transform into robots that start chasing you around the house, all the while the Transformers cartoon theme is playing in the background while, which would match up nicely with the current trend of everything being both terrifying and hilarious in a really bizarre way.