Well, yeah, that's because it's a piece of paper, not a calculator. More seriously, you have to be very careful "spooky action at a distance" in programming lan

Well, yeah, that's because it's a piece of paper, not a calculator. More seriously, you have to be very careful "spooky action at a distance" in programming language design. For example, you might say something like "Well, if the compiler can prove that every constant involved is provable in rational arithmetic, do that, otherwise use floating point arithmetic", which seems like a perfectly sensible thing to do, until you realize that it means that very small changes to the code will have drastic effects on the correctness of your program (if suddenly the compiler is no longer able to prove rational arithmetic is the same answer). We do have that sort of thing happen with performance in Julia (and in many other languages too, of course) - if the compiler can prove it can do something faster, it'll try to, but we try, very, very hard to give everything predictable, sequential execution semantics (i.e. you should be able to take code, run it step by step and generally get the same answer as if you had executed it all at once). One particular example of this is comprehensions. In early versions of julia, the type of `[f(x) for x in a]` would depend on what the compiler was able to prove about `f` (and some other things), e.g. if the compiler knew that `f` always returned an `Int`, you'd get a `Vector{Int}`, otherwise a `Vector{Any}` (or whatever the compiler could prove). This turned out to be hugely annoying to people because the semantics of the computation changed (slightly, only an eltype which you generally don't look at), depending on what the compiler was or was not able to prove about your program. These days, we have runtime semantics for non-empty comprehensions and only use static information to improve performance (which as I said before, we do anyway, so users are used to it). That's not to say that you couldn't do a language that changes semantics based on whole program analysis (you could probably do it in Haskell for example), but you'd lose part of the gradual transition from REPL to full program, which is very important to a system like Julia.