[dependenttypes]

> One issue not yet mentioned with Turing complete language at compile is that it makes tooling and IDE integration much more difficult

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.

[ImprobableTruth]

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

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

[touisteur]

The tractable replacement for a timeout is some kind of steps number. I thinks I've seen lots of long-running static-analysis tools use this for reproducible builds and results.

[qppo]

The analog of a timeout in a compiler is recursion depth limits.

[dllthomas]

Or just instruction count. Although in either case, while we are now machine agnostic (with some reasonable assumptions about the design) changing optimization flags that a build is running under might make it fail.

[ImprobableTruth]

That alone definitely won't suffice. A naïve fibonacci implementation will give you a recursion depth of n, but even fib(64) take ages.

[mikepurvis]

I don't think he's saying that a limit on recursion depth solves this problem. Rather, it's just a similar scenario where a real-world constraint (memory, time, whatever) comes to bear and may make a compilation fail on machine X where the identical code and environment would otherwise succeed on machine Y.

[ImprobableTruth]

Alright, but that's not a feature, right? Stack limitations are just a natural limitation. Timeouts are something that you'd intentionally introduce, when you don't necessarily need it. And if possible, I'd like to minimize dependency on specifics of the machine as much as possible.

[mikepurvis]

I dunno, I think they're pretty similar— both are an arbitrary cap that protects against exhausting a real world resource (time, memory).

In any case, the compile time evaluation would obviously still have a bunch of interesting constraints— like, probably reasonable to read in the contents of a file, but is it reasonable to make a network call? What about reading a file that's on a network share? Can you even tell the difference? That operation could also hang for reasons entirely outside of algorithmic complexity.

And of course, like a stack overflow, that's also true today; you can hang your compile by including a header from a network share that hangs.

So would it really be that bad to have the compilation hang, and just show a stack trace for the invoked-at-compile-time code when interrupted?

I don't think the halting problem is a deal breaker here.

[qppo]

It's not a limitation or the machine, it's a setting in the compiler.

Try doing anything pretty fancy at compile time with templates in C++ or macros in Rust and you'll quickly need to set the recursion depth limit higher.

[btilly]

A language that is Turing complete at compile means that an IDE cannot reliably tell whether code has a syntax error without running a program that can take arbitrarily wrong.

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.

[dependenttypes]

> A language that is Turing complete at compile means that an IDE cannot reliably tell whether code has a syntax error without running a program that can take arbitrarily wrong.

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.

[btilly]

It is possible to construct counterexamples, but in practice it tends to work out much, much better.

The various tools built around Java stand as an example.

[GolDDranks]

No, that's not true actually. It's possible that the language is defined so that the syntax checker (lexing, parsing, name resolution) and even type checker is run first and compile time execution after that. The only thing what the undecidability then affects is whether we get the constant value or whether the program runs forever. But in the latter case, we have still performed successfully syntax checking.