3 ms·

Well, they of course not defy computer science. The "trick" is that they are not Turing-complete, they mandate termination of every expression. Also, most of t

by gf000 8d ago

Well, they of course not defy computer science. The "trick" is that they are not Turing-complete, they mandate termination of every expression. Also, most of them are made to prove stuff first and foremost and thus trade off a lot of performance to the point that it makes them practically unusable for many stuff (e.g. numbers may be represented as an object that has n-1 further children recursively), though Lean is an exception as you note.

IsTom 8d ago
> The "trick" is that they are not Turing-complete, they mandate termination of every expression. I don't think this is a big deal for day-to-day programming. You're trying to stay in n, nlogn or maybe n^2 realm most of the time. And the kind of infinite loops you encounter (e.g. event loops) are co-inductive or have some notion of making progress.