I've been thinking about the best approach to implement pure function verification in the Scala compiler. An approach similar to the one in D would fit a lot better than the one used in Haskell (which would break all existing code and cause some problems due to strict evaluation). A solution using annotations would be quite simple to implement:
P. Wadler. FPCA '89: Proceedings of the fourth international conference on Functional programming languages and computer architecture, page 347--359. New York, NY, USA, ACM, (1989)