3 ms·
This sounds like Halide [1] which I think is also from the same group in MIT. However, Halide is an embedded DSL in C++. It sounds like ATL being based on Coq
by UncleOxidant 5y ago
This sounds like Halide [1] which I think is also from the same group in MIT. However, Halide is an embedded DSL in C++. It sounds like ATL being based on Coq would be more likely to always produce correct code.
[1] https://halide-lang.org/ https://halide-lang.org/
- downut 5y agoIndeed. Notice the last author. Halide has had transparent autodiff for some time now. I am guessing, this is follow-on work in the usual academic style. (Not trivializing at all.) I've been watching Halide for a while as I really like it, intuitively. Also it wasn't that hard to bring up on FreeBSD with a few patches, where it performs more or less exactly as on Linux when configured cpu only. That's solid generic programming, to say the least. However... I have no recent decades experience with HPC but I would be surprised if dense tensor operations were a significant component of current workloads. Could be though!