Is it possible to perform compile-time checks for all invariants?

Question

Static typing helps with compile-time checks for types. I'd like to know from the community here if it's possible to check for other types of invariants at compile-time?Let's say, I've got a function increase_balance(increment_value: int) but instead of allowing all possible integer values, I want the compiler to check that anytime this function is called, it is called with increment_value in the range 1 to 10000.Is it theoretically possible to do such checks at compile-time? I mean the compiler has to check every code path and verify that all code paths leading to increase_balance() leads to value that is neither = 10001. Is this is a problem that can be solved at compile-time? Does any programming language provide such features?While I've your attention, are there other such invariants you're aware of that can be checked during compile-time?

KsassPeuk · Accepted Answer

In all its generality, the problem is undecidable. But there are quite a lot of tools that are meant to formally verify properties about programs. Proof assistants, of course, but there are also tools for more mainstream languages, like Frama-C, Ada/Spark, Java/KeY, Creusot (Rust), etc.

edwcross · Answer

It _is_ possible to do some checks at compile time, but not for all programs. Or, you can check all programs, but only be _sure_ about your results on some of them. Or, you can add some constraints and force the programmer to write extra information so that you can make it work on more programs.
Overall, there's no free lunch: somewhere, someone will have to do some extra work.
Other useful invariants include some RAII idioms, Rust memory checks, resource usage (e.g. locks), etc.

stefanos82 · Answer

I could be wrong, but I have the impression what you are looking for is how constexpr and consteval work in C++ https://en.cppreference.com/w/cpp/language/consteval

Davidbrcz · Answer

You can look into theorem proover (Coq, lean ...) and code extracted from them. A middle ground is FramaC+WP plugin for hoare logic for C.Some languages like F* are also proof oriented.