zlacker

Proof assistants, which I expect to eventually merge with programming languages, can be used to restrict the set of programs you write to those where you can statically prove all properties you expect the program to hold. It’s not much different from what diligent programmers have always done in their head (with, of course, much more room for error).

The fact that arbitrary programs are undecidable is a red herring here.

>>layer8+(OP)
"Undecidable" Is way too close to your day2day program than you think: https://en.wikipedia.org/wiki/Rice%27s_theorem

I would like to learn otherwise, but even a React JS+HTML page is undecidable... its scope is limited by chrome V8 js engine (like a vm), but within that scope I don't think you can prove anything more. otherwise we could just make static analysis to check if it will leak passwords...

>>yonixw+sg
I’m not sure you understand Rice’s theorem correctly. It means that you can’t write an algorithm that takes an arbitrary program as input and tells you whether it fulfills a given nontrivial semantic property. But you can write an algorithm that can tell you for some subset of programs. So as a developer, if you restrict yourself to releasing programs for which the algorithm has halted and given you the desired answer, you are fine.

Depending on the semantic property to check for, writing such an algorithm isn’t trivial. But the Rust compiler for example does it for memory safety, for the subset of valid Rust programs that don’t use Unsafe.

>>layer8+6j
But isn't every program we write today (Rust, C++, Python, JS, etc.) raise up to the level of an "arbitrary program"? How do you find those "some subset of programs" that will halt by said algorithm?

The only sure way I can think of, is when you force your program to go through a more narrow non-turing algorithm. Like sending data through a network after Serialization. Where we could limit the De-Serialization process to be non Turing (json, yaml?).

Same for code, that uses non-turing API, like memory allocation in a dedicated per process space. Or rust "borrow" mechanics that the compiler enforces.

But my point is, everyday program are "arbitrary program" and not a red haring. Surly from the kernel perspective, which is Linus point imo.

>>yonixw+Nj
For the first question, see the second paragraph I added in my previous comment.

Regarding the second question, in the general case you have to guess or think hard, and proceed by trial and error. You notice that the analyzer takes more time than you’re willing to wait, so you stop it and try to change your program in order to fix that problem.

We already have that situation today, because the Rust type system is turing-complete. Meaning, the Rust compiler may in principle need an infinite amount of time to type-check a program. Normally the types used in actual programs don’t trigger that situation (and the compiler also may first run out of memory).

By the way, even if Rust’s type system wasn’t turing-complete, the kind of type inference it uses takes exponential time, which in practice is almost the same as the possibility of non-halting cases, because you can’t afford to wait a hundred or more years for your program to finish compiling.

> But my point is, everyday program are "arbitrary program"

No, most programs we write are from a very limited subset of all possible programs. This is because we already reason in our heads about the validity and suitability of our programs.

>>layer8+ym
> Regarding the second question, in the general case you have to guess or do trial and error.

> You notice that the analyzer takes more time than you’re willing to wait,

I see, thanks, didn't know about this feedback loop as I'm not a rust programmer. Still on my todo list to learn.

>>yonixw+do
I don’t think it actually happens in Rust in practice, or only very rarely. I was more talking about the hypothetical case for any static analysis of nontrivial program properties as in Rice’s theorem.

>>layer8+(OP)
> Rust is arguably less safe in that aspect than C, due to the general Rust practice of panicking upon unexpected conditions

For clarification, I responded to this in particular because "safety" is being conflated with "panicking" (bad for kernel). I reckoned "Unexpected conditions" means "arbitrary programs", hence my response, otherwise you could just remove the call to panic.