I've done quite a lot with the ML family, just not OCaml specifically. Type inference helps, but being able to use an Sexp-style representation a-la lisp is a huge, huge benefit in compilation. You cannot do this in any of the ML family.
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.
Yes, I'm aware. However, like most such things, they're simply not practical. Proving compiler correctness is insanely difficult (if it wasn't, we'd have much better compilers) and it very frequently ignores optimization entirely, making such compilers useless.
In theory, proving correctness is a good way to go. In the real world, it's not remotely viable.
Comments
I've done quite a lot with the ML family, just not OCaml specifically. Type inference helps, but being able to use an Sexp-style representation a-la lisp is a huge, huge benefit in compilation. You cannot do this in any of the ML family.
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.
There many attempts to get proofs for compilers for popular languages, C or Ada for example: http://portal.acm.org/citation.cfm?id=1315602 http://pauillac.inria.fr/~xleroy/publi/compiler-certif.pdf
Yes, I'm aware. However, like most such things, they're simply not practical. Proving compiler correctness is insanely difficult (if it wasn't, we'd have much better compilers) and it very frequently ignores optimization entirely, making such compilers useless.
In theory, proving correctness is a good way to go. In the real world, it's not remotely viable.