Program proofs can get arbitrarily clever/complicated.

But one of the fundamental maneuvers is to examine the full input space of a given function, and assert that the fully output space of a function has certain properties, which then may get fed in to later uses of the results of that function to further assert things.

The "full input space" of a function is generally what you'd expect it to be, but the "full output space" of a function is worth discussing. It is not just the return values of the function in the sense the local language means, it is also the full state of visible changes to the environment, any exceptions, etc. So, for instance, in the psuedocode function

// "int" is the conventional wrapping machine int here
function sample (int x, int y) int {
if (x == 25) {
throw DontLike25Error("I can't stand the number 25")
}
if (y == 0) {
external yZeros; // imagine I'm importing a global variable
yZeros++;
}
return x + y;
}

A human programmer will conceptualize this as "a function that sums two numbers with a weird bug", and probably ignore the yZeros entirely. A prover sees this as a function that "returns the exception DontLike25Error OR returns a new yZeros and the wrapped sum of the two input values". You generally conceive of exceptions as a return value, and global variable updates as a new value, etc.

So, if you want to prove a function will never divide by zero, it is at least conceptually a case of iterating over all possible inputs and verifying that the property holds that a DivideByZero exception is never returned:

function divide (num float, denom float) float {
if (denom == 0) {
return 0; // actually a bad idea, but bear with me
}
return num / denom;
}

We can now easily prove this never divides by zero, because we can examine all the possible nums and denoms and verify we always get a "float".

At least... if == 0 correctly detects all possible zeros, including the local negative zero if applicable, and doesn't return true for any other possible float value, and if the division operator doesn't yield a DivisionByZero for any other value accidentally or deliberately. And our proof system would still have to bear in mind the possibility of underflow (a non-zero numerator may still yield a 0 if the denominator is sufficiently large) or possibly an Inf overflow if the denominator is sufficiently small.

And with that paragraph, you begin to see both the problems with creating proof systems, and using them. We programmers want to slop down a division operator and assume that it's going to divide two numbers and yield a third number and we don't want to care about the exceptions. A proof system makes you care. As the program scales up, this only gets more interesting; the previous paragraph was just about one usage of the division operator. Pretty much every operator and function you've ever used comes with a similarly intense list of caveats, exceptions, and weirdnesses if you want to be really rigorous about what happens in your code. Especially including things like "allocating memory" or "allocating disk" as functions, which even before we're trying to prove things are often so difficult to deal with we programmers just punt entirely.

From these simple building blocks, you can start building you way up to more interesting assertions. But this is the foundation that the whole system is built on.

It's also worth pointing out that from this point of view, a prover is doing what even the sloppiest programmer is doing in their head anyhow. You have to at least to some extent be thinking about what goes into a function and exactly what comes out. You just probably aren't considering anywhere near all the options. But you must be thinking like this in some manner, no matter how incompletely and sloppily, to be a programmer at all. Proving things about code is less foreign than it should seem at first.

You can also even see how dynamic languages can start being difficult to deal with at scale if you don't apply a lot of discipline external to the dynamic language itself, because dynamically-typed languages have very "large" functions when you view them this way; with no way to constrain the inputs, it can be difficult to "range across all possible inputs" conceptually. This has perfectly practical real effects for things like tracing optimizing interpreters, which must in principle always be verifying incoming types to functions in a way a static language doesn't need to, no matter how optimized that check may be in practice.

You can put your toe into this world simply by learning how to use your type system to its maximum power. Type systems are in general not all that powerful compared to what a full prover can prove. (Not even Haskell's.) But it's a start, and it's relatively easy, and has good bang for the buck.

Incidentally, once you start looking at your code this way, it becomes obvious why functional programming is much easier to prove things about; in the purest case, you can't get surprise global variable updates and you don't get random unions of what can be returned by a function with things like "exceptions". You've got many fewer cases to worry about because the functions are what their type signature says they are, instead of their type signature unioned with a large set of exceptions unioned with arbitrary IO unioned with arbitrary global variable updates unioned with arbitrary code updates (in dynamic languages). However, this pretty image is often not fully realized; even Haskell can throw exceptions anywhere, even if it is discouraged. For math reasons, Haskell programmers say anything can be "bottom", which is this additional "crash" value that Haskell doesn't eliminate.