5 ms·
I agree that functional vs imperative is a red herring in this case. The Ethereum model is "imperative" anyway, so a functional DSL would probably end up looki
by mbrock 10y ago
I agree that functional vs imperative is a red herring in this case.
The Ethereum model is "imperative" anyway, so a functional DSL would probably end up looking like some kind of monad.
That said, it seems interesting to use a language like Agda for writing a DSL to EVM compiler, regardless of the exact nature of that DSL. Then you can have machine checked compiler correction proofs and also prove theorems about DSL programs.
- pron 10y agoThat would be interesting and even necessary. But why not use something much easier than Agda, though not less powerful for this use case -- like TLA+ -- something that even "ordinary" engineers could use to verify their contracts (not to mention that it supports model-checking in addition to deductive proofs, which reduces the verification effort considerably)?
- mbrock 10y agoMaybe that would be better. I admit that I don't know the first thing about TLA+. Agda is what I learned about in school, and what my computer science friends are excited about, and I was already interested in using it to write verified compilers. Writing compilers with functional languages was also a part of my university education. But that's just my background.
- willtim 10y agoI see parallels here with UI code that is very imperative in nature, but FRP and similar approaches are showing great promise in creating abstractions for reasoning.