compile to XLA?

Stream: lean4

[Jack B.]

Has any work been done on compiling lean to XLA?

[Mario Carneiro]

(https://openxla.org/xla) No. I don't even see how it would be applicable

[Jack B.]

JAX [3] (which compiles to XLA) directs the programmer to write pure functional programs in python and then compiles these to execute on GPU(s). Another research language (inspired by futhark [1]) called dexlang [2] has a similar flavor.

GPU programming is probably here to stay, so my question here is:

Can lean be engineered to generate performant GPU programs, emphasizing NLA? At the moment it seems like compiling lean to XLA would be the "best" or "most likely" path for this, but perhaps there are other routes.

[1] https://futhark-lang.org/
[2] https://github.com/google-research/dex-lang
[3] https://jax.readthedocs.io/en/latest/stateful-computations.html