[allenguo]

This was an interesting read. Thanks for sharing!

> This means that whenever I call this function, I need to provide together with a and b a proof that b isn’t zero.

What might such a proof look like? And is this supposed to work at compile-time?

[nbouscal]

Yes, it happens at compile time. To understand how proofs work here, you want to look at the Curry-Howard correspondence. Basically, there's a correspondence between types and propositions, and between the values inhabiting those types and proofs of the corresponding propositions. So a proof looks like a value of a certain type.