How so?
> When you need to run an unbounded program
How is a program that provably terminates but takes 2 years to finish any better for compile-time computation? You want timeouts in either case.
I'm not sure how realistic that actually is. Besides certain party tricks like encoding the ackermann functino using primitive recursion, I haven't actually seen anything like that. From my experience the vast majority of programs that don't finish in a reasonable amount of time are those that have some logic bug.
A timeout seems pretty off-putting. The idea that compilation could fail on a weaker machine just because it isn't fast enough just doesn't sit right with me.
The timeout should be set based on what the user of the machine considers acceptable. Why should I have to tolerate a 2 hour wait time for a compile-time computation to finish in order for the auto-complete menu to appear on emacs just because I am using a laptop from 2010?
> Besides certain party tricks like encoding the ackermann functino using primitive recursion, I haven't actually seen anything like that
Try prolog then (or something similar) and write something of the form sha512(X) = 0 this will initiate a brute-force search that will last essentially forever.
I don't understand. If you aren't willing to wait that amount of time, you're simply not getting working auto-complete at all. Hell, if you can't even compile the project, I don't see how you can meaningfully work on it all.
>Try prolog then (or something similar) and write something of the form sha512(X) = 0 this will initiate a brute-force search that will last essentially forever.
This is literally just another nonsensical party trick. I'm talking about something that someone might actually want to use, not contrived examples that really don't matter at all. I don't care to consider imaginary people that intentionally brick their programs.
You would want as much as possible to make the timeout not based on runtime -- but on an abstract model of the computation which doesn't actually depend on any machine particular. "Hey your program didn't compile on my machine -- try a faster cpu" would be a nightmarish interaction.
You want constraints about how long these programs are allowed to execute to be tight enough for developers to learn a sense for what is reasonable to do with these features -- as opposed to waiting for runtime.
All other tooling faces the same issue. What variables have a given type? If determining the type takes arbitrarily long, how are you supposed to discover them? Now consider the plight of an automated refactoring tool.
The IDEs and tools can still be written, of course. But they take more work and can't be as reliable.
A language that is not Turing complete at compile-time does not necessarily mean that an IDE will be able to reliably tell whether a certain piece of code has a syntax error without running a program that can take an arbitrarily amount of time to finish.
The various tools built around Java stand as an example.
