talk idea termination idris vs ethereum - benclifford/text GitHub Wiki

Two different notions of termination

idris

• prove termination
• don't care how long, as long as its finite
• needed for proof-like values that might never be computed
• avoid being allowed to pass in bottom as a value
• try to avoid you writing an infinite loop at compile time

ethereum

• provide "gas". you buy "gas" and your program runs till it runs out.
• can make some predictions about how long it will take but execution is in a context you don't fully know - eg there is block information, and the current time. However, you can still do analysis.
• you can write an infinite loop however it won't run forever.