Well, in a way, my vision is that Ethereum will *be* the future of general-purpose programming. That’s why it is mostly what I care about. But that’s, of course, that’s my personal (perhaps utopian) view. So, yes, this will be applied to “general-purpose” programming and people will be able to use the language to make anything.
That’s not the case! Perhaps you’re thinking in QuickCheck? Those are different. QuickCheck creates millions of random unit tests for you based on a specification. Formal proofs are a different beast: you mathematically prove the specification is correct. That is, suppose you want to prove that the function
f(x) = 2 * x, when given a natural number…
This is a cleaner specification of the idea, perhaps it may answer you.
It corresponds to a single “commute” rule on interaction combinators (check out the paper to see how it looks like). Basically, you rewrite 256 bits of memory (to replace 2 nodes), allocate 256 bits of memory (to create 2 new copies), then rewrite more…
Note that the Abstract Calculus can still copy almost anything. It can copy every non-high-order data structure. It can copy numbers, lists, hash-maps, trees and so on as much as you want. What you can not copy is a function which itself copies its arguments. So, for example, if you write something like:
foo(f, array)= (map(f, array), map(f, array))…
Converting the λ-calculus to abstract calculus can lead to wrong results (in terms of λ-calculus semantics). The whole point of this thing is that we can abandon λ-calculus semantics, though.xll
The depth is limited because otherwise I’d not be able to execute the non-copy version of the function, as its complexity becomes infinite (because, due to the fold-friendly way it is written, one must unfold the recursion before being able to apply it) and thus it never halts.
Ah, I think I can come up with simpler examples. Probably applying
copy to the result of a wide class of recursive functions achieves the same effect. I just didn’t have time to experiment yet. This may be the simplest explanation of the algorithm around, I believe, although it is not exactly simplistic language.