4 ms·

Thanks for a very thoughtful reply! (Feels like real HN. I appreciate that.) It seems like we're not in too much disagreement. I also see Rust's borrow checker

Thanks for a very thoughtful reply! (Feels like real HN. I appreciate that.) It seems like we're not in too much disagreement. I also see Rust's borrow checker as a real engineering achievement. They were able to take lessons learned discovering affine type systems and apply in in a way that gives Rust programs some tremendously wonderful properties. Whether it's making sure that the ML code doesn't do something invalid or whether all of the code doesn't make memory errors, I still see a never-ending march of progress on investing more into type systems and static analysis. I appreciate your insights on Physics. I understand enough that Quantum Physics takes the view (more or less, I believe!) that the universe is akin to a computer, with particles (bits) that behave in specific ways and determine how everything works (computation, if I can continue the metaphor). I replied to your linked comment. But I think there's perhaps a misunderstanding of what types are. I agree: units aren't types. However, a > a property of a physical system based on some model counts as a value that has a type. Perhaps the whole understanding is that Physics has a _very complex type system_. Perhaps one that no one has invested in trying to make computable?

tsimionescu 3y ago
Yes, I think we agree quite a bit, and for me as well this is exactly the type of conversation I come to HN for. I replied more in depth on the measurement units post on the specifics about that, so I'll leave it aside here. > I appreciate your insights on Physics. About physics though, I would say that when I'm talking about computations I'm not describing some complex or deep idea about the universe acting as a computer. I just mean that most of what you do as a physicist is simply to do computations, much like we would in school. You don't write proofs the way most mathematicians do: you take some functions (say, Newton's laws of motion) and an initial state, and compute the state of the system after some time or at some event. Your result is not a proof that X = Y, it is simply the value Y, which you didn't know beforehand. Ideally, you might write a program that automates this work for you, so that instead of doing a computation by hand, you ask a computer to do it for you. > But I think there's perhaps a misunderstanding of what types are. I agree: units aren't types. However, a >> a property of a physical system based on some model > counts as a value that has a type. I don't think this is the right way to look at it. Types are a specific concept in computer science/math and they act in certain ways. They are for example isomorphic to propositions in first order logic (the Church-Howard correspondence if I remember correctly), but that doesn't mean they are the same thing.

tsimionescu 3y ago

Yes, I think we agree quite a bit, and for me as well this is exactly the type of conversation I come to HN for. I replied more in depth on the measurement units post on the specifics about that, so I'll leave it aside here. > I appreciate your insights on Physics. About physics though, I would say that when I'm talking about computations I'm not describing some complex or deep idea about the universe acting as a computer. I just mean that most of what you do as a physicist is simply to do computations, much like we would in school. You don't write proofs the way most mathematicians do: you take some functions (say, Newton's laws of motion) and an initial state, and compute the state of the system after some time or at some event. Your result is not a proof that X = Y, it is simply the value Y, which you didn't know beforehand. Ideally, you might write a program that automates this work for you, so that instead of doing a computation by hand, you ask a computer to do it for you. > But I think there's perhaps a misunderstanding of what types are. I agree: units aren't types. However, a >> a property of a physical system based on some model > counts as a value that has a type. I don't think this is the right way to look at it. Types are a specific concept in computer science/math and they act in certain ways. They are for example isomorphic to propositions in first order logic (the Church-Howard correspondence if I remember correctly), but that doesn't mean they are the same thing.