Scale By the Bay Scale By the Bay

Shape safety in tensor programming is easy for a theorem prover

- PDT
functional

Peng Cheng
Schedule One, Lead Engineer

Peng love to exploit distributed computing frameworks for all kinds of weird things, from cryptography with hypersegmentation (DataPassports - 2015) to drone swarm (spookystuff-UAV - 2017). Most recently, he started pursuing his grail: to reclaim scala's acceptance among machine learning engineers from the great serpent


We present shapesafe (https://github.com/tribbloid/shapesafe) - the most comprehensive compile-time verifier for scala linear algebra - by only exploiting scala's type system as a theorem prover. This new paradigm allows type-level tensor computations, even those as complex as composite neural network blocks, to be rewritten, simplified and verified while being written. We will talk about its design and limitations, and most important, what we have observed and learned from it