[dependenttypes]

> 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.

[ImprobableTruth]

>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?

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.

[dependenttypes]

I just realized that you said "are those that have some logic bug" rather than "are those that due to a logic bug loop forever" and also mentioned that this is true for the "vast majority of programs" in which case.. sure? If anything this is an argument that supports timeouts and can happen in both turing-complete and non-turing complete languages, plus I do not understand how popularity has anything to do with it.

> If you aren't willing to wait that amount of time, you're simply not getting working auto-complete at all

Or I am getting a working auto-complete for code that does not make the completion system to get killed by the timeout.

> Hell, if you can't even compile the project

I never mentioned not being able to compile the project.

[breatheoften]

A user configurable parameter for timeout would be a terrible language design mistake.

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.

[dependenttypes]

So, the user should not have the option to say "hey, I want this done within 10 minutes because I have to leave soon" or "I want my auto-complete to be done within 1 second", got it. Instead we should care about the feelings of arm and atom cpus.