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 uni

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.