That particular thesis actually ends up recommending against using a dependent functional language for Ethereum contracts...
I think we might need to think of contracts as very important algorithms and prove them like we prove quick sort. That doesn't require dependent typing and functional programming; you can prove theorems about imperative code if you just have formal semantics.
I'd be interested to see a verified dependently typed compiler to EVM for some simple language... but it kind of seems like a PhD project.
I think we might need to think of contracts as very important algorithms and prove them like we prove quick sort. That doesn't require dependent typing and functional programming; you can prove theorems about imperative code if you just have formal semantics.
I'd be interested to see a verified dependently typed compiler to EVM for some simple language... but it kind of seems like a PhD project.