4 ms·

I think part of the argument is that if you want to have confidence in the correctness of a system, the system has to be so small and simple that anyone can ful

I think part of the argument is that if you want to have confidence in the correctness of a system, the system has to be so small and simple that anyone can fully understand it and keep it all in their head. For example, how do you know that the toolchains for Rust, Spark, sel4 work correctly? Have all aspects been verified or proven? Can a single person fully understand them? I’m not saying that’s the necessarily best criterion. The point is that all the guarantees that Rust, spark, Haskell, etc give are only meaningful if you can trust the tools to correctly implement them. Simplicity of the tools is one approach.

MaxBarraclough 6y ago
> how do you know that the toolchains for Rust, Spark, sel4 work correctly? Have all aspects been verified or proven In the case of Sel4, yes. The ARMv7 assembly code has been shown to be free of bugs. [0][1] SPARK Ada does not have a formally verified compiler, but there are various Ada compilers that are approved for use in life-and-death applications. The Boeing 777 flies on Ada code, for instance. [2] To my knowledge, compiler bugs aren't a major practical concern for SPARK, although a formally verified compiler would be a great addition. C has a fully verified compiler in CompCert. [3] I know of no other language with a fully verified compiler. (CompCert supports almost all C features, so it will either produce a valid binary for the input C code, or else fail with an error.) Rust has a bit of a history of troublesome compiler bugs. I think we're a way off seeing Rust used in critical systems, assuming it would even make sense to use a language like Rust. Memory management is handled quite differently in applications like avionics. > Can a single person fully understand them? The compilers/linkers? I imagine the most well-informed developers on the Rust and Ada compilers pretty much know how everything works, but really that's just a guess. If someone were to make a compiler specifically for SPARK, it could be simpler than a full Ada compiler, as SPARK forbids most Ada features. I don't know that this is likely to happen though. [0] https://docs.sel4.systems/projects/sel4/frequently-asked-questions.html https://docs.sel4.systems/projects/sel4/frequently-asked-que... [1] https://sel4.systems/Info/FAQ/proof.pml https://sel4.systems/Info/FAQ/proof.pml [2] http://archive.adaic.com/projects/atwork/boeing.html http://archive.adaic.com/projects/atwork/boeing.html (This is about Ada, and is not specifically about the SPARK subset) [3] https://en.wikipedia.org/wiki/CompCert https://en.wikipedia.org/wiki/CompCert

MaxBarraclough 6y ago

> how do you know that the toolchains for Rust, Spark, sel4 work correctly? Have all aspects been verified or proven In the case of Sel4, yes. The ARMv7 assembly code has been shown to be free of bugs. [0][1] SPARK Ada does not have a formally verified compiler, but there are various Ada compilers that are approved for use in life-and-death applications. The Boeing 777 flies on Ada code, for instance. [2] To my knowledge, compiler bugs aren't a major practical concern for SPARK, although a formally verified compiler would be a great addition. C has a fully verified compiler in CompCert. [3] I know of no other language with a fully verified compiler. (CompCert supports almost all C features, so it will either produce a valid binary for the input C code, or else fail with an error.) Rust has a bit of a history of troublesome compiler bugs. I think we're a way off seeing Rust used in critical systems, assuming it would even make sense to use a language like Rust. Memory management is handled quite differently in applications like avionics. > Can a single person fully understand them? The compilers/linkers? I imagine the most well-informed developers on the Rust and Ada compilers pretty much know how everything works, but really that's just a guess. If someone were to make a compiler specifically for SPARK, it could be simpler than a full Ada compiler, as SPARK forbids most Ada features. I don't know that this is likely to happen though. [0] https://docs.sel4.systems/projects/sel4/frequently-asked-questions.html https://docs.sel4.systems/projects/sel4/frequently-asked-que... [1] https://sel4.systems/Info/FAQ/proof.pml https://sel4.systems/Info/FAQ/proof.pml [2] http://archive.adaic.com/projects/atwork/boeing.html http://archive.adaic.com/projects/atwork/boeing.html (This is about Ada, and is not specifically about the SPARK subset) [3] https://en.wikipedia.org/wiki/CompCert https://en.wikipedia.org/wiki/CompCert