3 ms·
Holy smokes, that Z3 prover for Nim programs with inline invariant conditions is mindblowing, thank you for sharing this. Also, your username looked familiar -
by gavinray 6y ago
Holy smokes, that Z3 prover for Nim programs with inline invariant conditions is mindblowing, thank you for sharing this.
Also, your username looked familiar -- you're the creator of Arraymancer and Laser!!
You wrote the most performant, memory-efficient fast-math libs in existence currently (as far as I know) and your work on data-parallel operations is super fascinating.
- mratsim 6y agoThanks for the kind words, I think that crown is for MKL-DNN / OneDNN though, for now ;), and in the deep learning domain. I also expect Halide[1], Taichi[2], DaCe[3] and Tiramisu[4] to be able to more easily reach those levels of performance hence why I want to add a compiler to Laser (implemented at compile-time via Nim macros) but prerequisite is excellent and composable multithreading support which OpenMP didn't provide. In statistics / data analysis, my PCA though (Principal Component Analysis) beats all implementations I've seen from Scipy, Facebook and R. [1]: https://halide-lang.org/ https://halide-lang.org/ [2]: https://github.com/taichi-dev/taichi https://github.com/taichi-dev/taichi [3]: https://github.com/spcl/dace https://github.com/spcl/dace [4]: http://tiramisu-compiler.org/ http://tiramisu-compiler.org/
- gavinray 6y agoI had seen Taichi (still not entirely sure what "Differentiable Computing" is!) and Tiramisu before but not Halide or DaCe. Neat =D For whatever it's worth, Arraymancer was #1 on Matmul benchmark (no claims to it being a realistic measure of realworld implementation) until what must have been only the last few weeks: https://github.com/kostya/benchmarks#matmul https://github.com/kostya/benchmarks#matmul At some point recently that D lang library snuck in the top spot.