4 ms·

In fact, I say Rust didn't go far enough. https://gavinhoward.com/2024/05/what-rust-got-wrong-on-formal-verification/ https://gavinhoward.com/2024/05/what-rust

• two_handfuls 2y ago
  One thing I don’t understand there is why you say it’s ok for a function to return a value, but bad for it to return code (async or thread). What makes it bad? How does it make harder to prove properties of the program?
  • gavinhoward 2y ago
    Because it can make an assumption that the data will do nothing once it is returned. Sure, code is data (I've written Lisp before), but code isn't just Plain Old Data because it can do stuff.
    • two_handfuls 2y ago
      Would a function pointer be equally bad in your book?
      • gavinhoward 2y ago
        Yes.
        • two_handfuls 2y ago
          What property can’t we prove if we have function pointers? The article mentions trying to prove local properties of functions, and that’s all well and good, and similarly we could prove local properties of the function being pointed to. I guess what I’m saying is I think I’m missing something about why you are advocating removing those. It’s not just so we can statically prove that all destructors are called is it?
          • gavinhoward 2y ago
            Function pointers are not the problem. Returning function pointers is the problem. And the problem is that we don't know if the caller will run that code or not, but if they do, that code is not in the subprogram anymore. You can pass function pointers to callees, no problem.
            • two_handfuls 2y ago
              Ok, the problem is we don’t know whether that code will be called. So if we added some way to require that value to be used, something similar to `std::hint::must_use`, then we may be able to return function pointers?
              • gavinhoward 2y ago
                No, because we also don't know what the program does if it is called because it is Turing-complete.
                • two_handfuls 2y ago
                  I’m confused. That also holds for functions that don’t return a function pointer, so this cannot be a good argument for banning returning function pointers.
                  • gavinhoward 2y ago
                    By program, I mean the function pointer. The caller is not part of the subprogram, but the returned function pointer is, and if the caller runs it, it leaks out, in the same way async and other things do.