4 ms·

> But a specification doesn't need to be written in English, it can be written as a formal proof, and indeed I would expect a theoretical Rust spec to specify t

> But a specification doesn't need to be written in English, it can be written as a formal proof, and indeed I would expect a theoretical Rust spec to specify the behavior of the borrow checker as just such a proof. Did you miss the part where the person you're responding to mentioned Rice's theorem? Do you know Rice's theorem and hence understand what they're implying?

Ygg2 2y ago
Rice theorem doesn't say anything about humans.
- almostgotcaught 2y ago
  No clue what this means
  - tialaramex 2y ago
    Some people believe that the Church-Turing intuition doesn't tell us anything about humans, that what humans are doing isn't computation but something more powerful. In my experience their lack of evidence for this belief just makes them believe it even harder, and they often write whole books which are in effect the argument from incredulity but expanded to book form.
    - carbotaniuman 2y ago
      There is no proof that humans are just glorified Turing machines and even as a nonreligious person, I find such a statement to be as lacking in evidence as those that claim humanity has some soul or similar that cannot be replicated. The actual logic of gggp's statement also doesn't make any sense. We as humans also under and overestimate the soundness of programs. Sometimes, a perfectly fine solution is massaged to better adhere to best practices because we can't convince ourselves that it's correct. Rust requires that we convince the compiler, and then we know it's correct via the compiler's proofs, instead of requiring us to do the proof all the time.
      - IshKebab 2y ago
        > I find such a statement to be as lacking in evidence as those that claim humanity has some soul or similar that cannot be replicated. It doesn't need evidence; it is the null hypothesis. Brains clearly compute, and it appears that computation is sufficient to produce the observed behaviour of brains. All our experience of the universe and physics suggests that there is no magic or metaphysics or souls or whatever. So the onus is on you to show that there's something more going on. It isn't a 50:50 "is it heads or tails", it's more like "I claim that the tooth fairy exists" vs "I'm pretty sure it's your mum".
    - Ygg2 2y ago
      It's simpler than this. Turing machines are a beautiful abstraction. Whatever happens in humans is much, much, much, much, much, much messier, on the account of it being subject to laws of evolution and working on a scale where various micro-effects can be felt (radiation, Brownian motion and quantum effects anyone?). So even if the Turing machine model is correct (and we don't know that), it's overtly simplified.
  - Ygg2 2y ago
    Humans are not Turning machines. I'm not talking how we work on fundamental level. I'm saying we don't obey axioms of Turing machine model. So Rice theorem nor Godel theorem can apply to unsafe code written by humans. Even if borrow checker is limited by the Rice theorem, you can create either safe abstractions provably or unsound abstractions provably or potentially unsound abstractions, which humans can reject or accept.
kibwen 2y ago
Rice's theorem isn't relevant here. The goal is not to create a system that produces no false positives, it's perfectly fine to do a conservative syntactic analysis that allows false positives but disallows false negatives, and it's then possible to produce a formal proof that this analysis is sound. It is this formal proof that I would expect to be included in a specification in lieu of English prose.
- tialaramex 2y ago
  Sure, there's a reason I said "Extremely difficult" not "Impossible". Defying Rice without losing generality is mathematically impossible. This is on that continuum where it's definitely neither impossible nor easy enough that we can just let some bored grad student knock out the answer, and so now somebody who wants this must do lots of hard work. I think a specification which says e.g. here's the semantic requirement, here's a rule for scoped borrows which works, you must do at least that, but you can do more however you must not allow anything which violates the semantic requirement - would be great, but if you had that rule in your standard then people can write conforming Rust programs which don't compile - they need a yet-to-be-written smarter compiler to figure out why they're legal, which is kinda annoying as a language feature.

Ygg2 2y ago

Rice theorem doesn't say anything about humans.

almostgotcaught 2y ago
No clue what this means
- tialaramex 2y ago
  Some people believe that the Church-Turing intuition doesn't tell us anything about humans, that what humans are doing isn't computation but something more powerful. In my experience their lack of evidence for this belief just makes them believe it even harder, and they often write whole books which are in effect the argument from incredulity but expanded to book form.
  - carbotaniuman 2y ago
    There is no proof that humans are just glorified Turing machines and even as a nonreligious person, I find such a statement to be as lacking in evidence as those that claim humanity has some soul or similar that cannot be replicated. The actual logic of gggp's statement also doesn't make any sense. We as humans also under and overestimate the soundness of programs. Sometimes, a perfectly fine solution is massaged to better adhere to best practices because we can't convince ourselves that it's correct. Rust requires that we convince the compiler, and then we know it's correct via the compiler's proofs, instead of requiring us to do the proof all the time.
    - IshKebab 2y ago
      > I find such a statement to be as lacking in evidence as those that claim humanity has some soul or similar that cannot be replicated. It doesn't need evidence; it is the null hypothesis. Brains clearly compute, and it appears that computation is sufficient to produce the observed behaviour of brains. All our experience of the universe and physics suggests that there is no magic or metaphysics or souls or whatever. So the onus is on you to show that there's something more going on. It isn't a 50:50 "is it heads or tails", it's more like "I claim that the tooth fairy exists" vs "I'm pretty sure it's your mum".
  - Ygg2 2y ago
    It's simpler than this. Turing machines are a beautiful abstraction. Whatever happens in humans is much, much, much, much, much, much messier, on the account of it being subject to laws of evolution and working on a scale where various micro-effects can be felt (radiation, Brownian motion and quantum effects anyone?). So even if the Turing machine model is correct (and we don't know that), it's overtly simplified.
- Ygg2 2y ago
  Humans are not Turning machines. I'm not talking how we work on fundamental level. I'm saying we don't obey axioms of Turing machine model. So Rice theorem nor Godel theorem can apply to unsafe code written by humans. Even if borrow checker is limited by the Rice theorem, you can create either safe abstractions provably or unsound abstractions provably or potentially unsound abstractions, which humans can reject or accept.

kibwen 2y ago

Rice's theorem isn't relevant here. The goal is not to create a system that produces no false positives, it's perfectly fine to do a conservative syntactic analysis that allows false positives but disallows false negatives, and it's then possible to produce a formal proof that this analysis is sound. It is this formal proof that I would expect to be included in a specification in lieu of English prose.

tialaramex 2y ago
Sure, there's a reason I said "Extremely difficult" not "Impossible". Defying Rice without losing generality is mathematically impossible. This is on that continuum where it's definitely neither impossible nor easy enough that we can just let some bored grad student knock out the answer, and so now somebody who wants this must do lots of hard work. I think a specification which says e.g. here's the semantic requirement, here's a rule for scoped borrows which works, you must do at least that, but you can do more however you must not allow anything which violates the semantic requirement - would be great, but if you had that rule in your standard then people can write conforming Rust programs which don't compile - they need a yet-to-be-written smarter compiler to figure out why they're legal, which is kinda annoying as a language feature.