News for hackers. Stuff that matters.

A comment on Programming Languages Going Above and Beyond. Parent comment

Re:Programming Languages Going Above and Beyond by thr_ddv on Thursday June 29, 2023 @03:49PM (#36525779)
>The compiler still cannot tell when our loops will terminate (yes, this is possible).

    while(n < busy_bever(10))
        n++
Tell me when my loop terminates.
[ Parent | on HN ]
Re:Programming Languages Going Above and Beyond by jcranmer on Thursday June 29, 2023 @04:33PM (#36526304)
Assuming you meant 'busy_bever' to implement the busy beaver function, said function is in fact not a computable function, which means you can't write it down in a programming language.
[ Parent | on HN ]
Re:Programming Languages Going Above and Beyond by Smaug123 on Thursday June 29, 2023 @05:40PM (#36527137)
This is true but somewhat misleading. The nth busy beaver numbers are known for n <= 4. It's within the bounds of possibility that we will some day learn the nth busy beaver numbers for n <= 10. (What we can say is that the parent's loop will never terminate for any known definition of "ever" that pertains to the physical universe.)
[ Parent | on HN ]
Re:Programming Languages Going Above and Beyond by jjnoakes on Thursday June 29, 2023 @04:30PM (#36526261)
> Tell me when my loop terminates.

I think the point is that even though one can't determine loop termination for all loops (easily provable), there are a huge number of useful loops that do useful work and for which you can prove properties like termination (and other static properties).

[ Parent | on HN ]
Re:Programming Languages Going Above and Beyond by redjamjar on Thursday June 29, 2023 @05:06PM (#36526695)
> there are a huge number of useful loops that do useful work and for which you can prove properties like termination

Exactly! If the loop doesn't terminate, then you obviously cannot show it. But if it does, then you should be able to (even if that requires some changes to help the tool)

[ Parent | on HN ]
Re:Programming Languages Going Above and Beyond by jjnoakes on Thursday June 29, 2023 @06:26PM (#36527681)
> If the loop doesn't terminate, then you obviously cannot show it.

I don't think this is true for all loops either - some can be proven to never terminate, just like some can be proven to terminate. And some can't be proven either way.

[ Parent | on HN ]
Re:Programming Languages Going Above and Beyond by redjamjar on Thursday June 29, 2023 @06:33PM (#36527759)
Yeah, ok that’s fair enough!!
[ Parent | on HN ]
Re:Programming Languages Going Above and Beyond by rockstar-guy-23 on Thursday June 29, 2023 @03:57PM (#36525863) 

    while(calculate_pi_stream(10 /* substring length */) != 0987654321);
[ Parent | on HN ]
Re:Programming Languages Going Above and Beyond by redjamjar on Thursday June 29, 2023 @05:07PM (#36526714)
Haha, yeah ... this one you would have a very hard time with :)

Hopefully, though, termination of your program does not depend on this ... otherwise could be a long wait!

[ Parent | on HN ]
Re:Programming Languages Going Above and Beyond by nine_k on Thursday June 29, 2023 @05:22PM (#36526908)
I remember there was a theorem that one can find an arbitrary substring in a long enough output of infinite (stationary) random process. I also suppose that a decimal representation of pi may count as one, then your function provably terminates.

But this is of a theoretic interest. In practice the verifier says: "I can't prove that this function will terminate within (some reasonable window), program rejected". And this is what's actually needed: a program that provably has certain properties, where an automatic proof is tractable.

[ Parent | on HN ]
Re:Programming Languages Going Above and Beyond by xigoi on Thursday June 29, 2023 @06:32PM (#36527748)
It is currently not known whether π is a normal number (that is, its representation in any base contains any finite sequence of digits with the same density as in a uniformly random string of digits).
[ Parent | on HN ]
Re:Programming Languages Going Above and Beyond by littlestymaar on Thursday June 29, 2023 @03:54PM (#36525828)
That's not a very good exemple because with BB we know the code terminates, by definition. The canonical tong-in-cheek argument is to use the Collatz conjoncture instead (but even that isn't a good example in practice: https://news.ycombinator.com/item?id=21440306)
[ Parent | on HN ]
Re:Programming Languages Going Above and Beyond by thr_ddv on Thursday June 29, 2023 @03:56PM (#36525853)
I'm not asking if it terminates, I'm asking when it does. After all it's not much use if the number overflows the universe.
[ Parent | on HN ]
Re:Programming Languages Going Above and Beyond by littlestymaar on Thursday June 29, 2023 @04:37PM (#36526364)
But that's not something these kinds of tools are supposed do, even with trivial functions… These tools have no idea about the run-time (and there's no way they coule, since it depends on the load you put on the hardware in parallel of running your program)
[ Parent | on HN ]
Re:Programming Languages Going Above and Beyond by redjamjar on Thursday June 29, 2023 @05:10PM (#36526748)
I agree. There are tools though which are specifically for determining worst-case execution time for e.g. embedded systems which can actually give accurate timing information (upto a point).
[ Parent | on HN ]
Re:Programming Languages Going Above and Beyond by redjamjar on Thursday June 29, 2023 @05:09PM (#36526730)
Yeah, so these tools will not tell you how long it will take to terminate --- only that it will eventually. In the vast majority of cases, that is what you want to know.
[ Parent | on HN ]
Re:Programming Languages Going Above and Beyond by nine_k on Thursday June 29, 2023 @05:25PM (#36526948)
For practical reasons, it's enough to prove that it takes longer than some upper bound, say, 10 ms. The rest is not important.
[ Parent | on HN ]