[baddox]

There are lots of attributes that are provably impossible to statically determine about a computer program. Whether the program halts is the obvious example, but Rice's theorem generalizes this to effectively any attribute of a computer program you would be likely to care about.

https://en.wikipedia.org/wiki/Rice%27s_theorem

[TheCoelacanth]

Impossible to prove for any arbitrary program doesn't mean impossible to prove for programs that we actually care about, and it especially doesn't mean impossible to prove for a program where the programmer is intentionally trying to write a program where certain attributes are provable.

Any statically typed language necessarily has to prevent some well-formed programs from being represented. This language would just need to reject programs where it can't prove the attributes that it is suppose to prove in addition to programs that are actually malformed.

It is really ergonomics that prevents a language like this from taking off, not any theoretical concerns. Languages that let you prove a lot of complex properties at compile-time take too much work to use, but they are not impossible to create.

[ghayes]

F-Star [0] and Idris [1] are two great languages which give you a large variety of static analysis, and yes, provide ways to prove totality.

Idris, for instance, disallows recursion unless it can prove an argument "smaller" in the recursive call. For instance:

    fib : Nat -> Nat
    fib Z = Z
    fib (S Z) = (S Z)
    fib (S (S n)) = fib (S n) + fib n 

In this case, the function pattern matches on natural numbers (Z stands for Zero and S for the one plus some other natural number). Each recursive call of `fib` has an argument which is smaller (closer to the base case), and thus this program must halt. Idris will not compile unless it can prove the program will halt. It, therefore, rejects all programs which would have halted but which it could not prove.

[0] https://www.fstar-lang.org/

[1] https://www.idris-lang.org/

[dwohnitmok]

Rice's Theorem generalizes this to any implementation-independent attribute (i.e. properties of the idealized function on natural natural numbers a program represents). However, certain implementation-specific details such as run time (i.e. performance) are fair game. In particular it is quite simple to at least calculate lower bounds on run time. Simply choose a lower bound and then run the program and see if it halts before then.

[baddox]

If you can do that with your program then you can probably just precompute the actual result at build time. Many, if not most unexpected performance problems occur with unexpected or unconsidered inputs.

[dwohnitmok]

There are far less wasteful ways of calculating implementation-specific details. My "run until completion" was just an existence proof that general techniques exist. Things like symbolic execution, type systems, and other static analysis tools could in theory help here.

That being said I have personally yet to see non-toy static analysis tools for performance (although I suspect they exist at least in some limited fashion or operating in some constrained domains). This is probably due to the nature of certain pathological inputs and code paths as you point out.

There may nonetheless be hope if you guide the way users can write programs as a sibling comment points out.

[alexisread]

There are many properties as such, but we can still prove many properties about a program despite non-deterministic behaviour, using hidden logic https://cseweb.ucsd.edu/~goguen/pps/hherb.ps

As such, a proof system which incorporates behavioural specification is highly desirable.