2. Having never used OCaml for compiler dev, I can't speak on this.
3. The lack of strong typing has no effect on the ability of Python or Ruby to handle compilation. Like the Lisp family, these are very, very flexible languages with strong benefits to compiler developers, and I wouldn't trade them for anything else I've used.
TBH, I think ML-based languages are poor choices for compiler development. You spend as much time worrying about your own code as you do the code you're compiling, which you just don't do when you write a compiler in Scheme, Ruby, or another 'dynamic' language.
Pattern matching is a great feature, and it's available in all of the languages I mentioned. It's a built-in in Boo, there are many libraries for it in Scheme, and I have my own Sexp pattern matching libraries for Python and Ruby. It may have come from the ML world, but it's by no means exclusive to it.
As for proving correctness, depending on the language to provide this is simply not realistic in compilers. You've got a much better shot at correctness by making your compiler easier to work on, IMO.
In theory, proving correctness is a good way to go. In the real world, it's not remotely viable.
During the compilation? Would you even see the difference if the compiler did 0.1*0.2 by emulating cpu processing, instead of via one instruction? The cost of register allocation for a simple function will be greater than optimising many constant fp expressions. It simply doesn't matter here. If you have a convenient type, you use it, if you don't, you download any libieee754 and interface with its functions...
Seriously - if you're writing a compiler, there are so many more important problems than lack of mapping between the target and local types :( It may not be an elegant solution to handle fp expression evaluation via an external library, but it's only done during the compile time (so only once) and it's easily solvable.
(Not that this would stop the GNU people. Have you seen the code from bison? They actually emit code for their own reimplementation of memcpy() on some platforms. They are fanatical about compatibility. Or they were last time I checked. Which was sometime during the 90s.)