News for hackers. Stuff that matters.

A comment on Writing a compiler in Python using Lex, Yacc and LLVM. Parent comment

Re:Writing a compiler in Python using Lex, Yacc and LLVM by daeken on Saturday September 19, 2009 @10:33PM (#832629)
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.

[ Parent | on HN ]
Re:Writing a compiler in Python using Lex, Yacc and LLVM by ilkhd2 on Saturday September 19, 2009 @11:46PM (#832681)
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
[ Parent | on HN ]
Re:Writing a compiler in Python using Lex, Yacc and LLVM by daeken on Saturday September 19, 2009 @11:49PM (#832684)
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.

[ Parent | on HN ]