Llvm has come up as a suggestion a number of times. I did look at it
some years ago as a possible back-end for Poly/ML and came to the
conclusion that it wouldn't work in the way that was needed. I read the
blog post about GHC and thought it was interesting that they still felt
the need to have their own back-end as well.
The problem I could see was that Llvm seems to have its own ideas about
data representation and that wouldn't fit with the way Poly/ML works
especially in Isabelle. I could see a possible use for it as a back-end
when Poly/ML was batch-compiling some ML code to be executed as a
separate program.
However, interactive theorem proving in Isabelle is more like
manipulating data structures some of whose elements happen to be blobs
of executable code. This fits with the view of a functional language in
which functions are just another kind of value. The Poly/ML compiler,
just another function in the environment, builds code in the heap and if
the heap is saved to disc only then will the code be written out. That
is quite different from the conventional view of a compiler.
I'm quite happy to provide any information needed if someone wants to
look at an Llvm back-end but I don't see it working with Isabelle.
David
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
