You don't reason about the bits churned out by a compiler but about the actual code you write. If you want to preserve such information during the compilation process, you probably want to run the compiler without any optimization flags at all.
At the moment, with the way you are thinking about it, you'd have to reason about every program based on every compiler version it can go through. What happens instead is that people prove their program correct and other people prove the compiler correct. What it does behind the scenes doesn't matter: it's meant to preserve the exact semantics and if it does extra stuff on top that doesn't change those (like optimisation) you should be happy as now it will run more efficiently in practice, and not just on paper. On 06/02/13 11:45, Jan Stolarek wrote: > programmer wouldn't be able to reason about space behaviour of a > program _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe