Comment by asparagui
11 hours ago
Very cool! I have been using Lean to drive PJRT like so: https://github.com/brettkoonce/lean4-mlir and in theory your code could unlock another platform!
11 hours ago
Very cool! I have been using Lean to drive PJRT like so: https://github.com/brettkoonce/lean4-mlir and in theory your code could unlock another platform!
Thanks for sharing, this is super cool! Right now my approach to correctness it to just run as many tests as possible and fix them (torchtpu greatly expands the amount of available tests), but formal verification is also super cool. Having a look at your book https://lean.brettkoonce.com/blueprint.pdf
The Tenstorrent ISA is documented btw https://github.com/tenstorrent/tt-isa-documentation, I wonder if one could do the verification end-to-end with the hardware.