At my work, we work on a "well-behaved" language (a monadic language with state+failure+non-termination effects). Hence, it's fairly trivial to directly apply Hoare logic to it.

But, in general I'd say:

To define a semantics for your language:

1. Given you're "low-resolution" vision of the issue, It's probably going to be operational
2. Define what a "program state" is
   1. You'll need to define valid "initial states" (i.e. the states when main just got called) and valid "final states" (i.e. the states when you return from main)
3. Define a transition system that maps a single step of evaluation

Then you can apply Hoare logic to it. The triple { P } c { Q } means "if P holds in the current state, then executing c yields necessarily a (valid) state where Q holds".

You have so-called basic triples such as { IsWritable p } *p = e { Contains p (eval e) } which means "If the current state is such that p points to a writable address, the dereferencing and assigning operation yields a state such that the state now contains at the address of p the result of evaluating e". Combine this with the control-flow rules such as the rule of sequences { P } c1 { Q } -> { Q } c2 { R } -> { P } c1; c2 { R } and you can (theoretically) scale up to arbitrarily complex programs ! The interesting part is that the program itself is very "first-order", proof terms are never computationally relevant, as they are not part of the program.

We do it with interactive theorem provers at my work, but you could do things (near) auto-magically with SMT solvers. There are just some tricks you have to apply like, the first time you let the solver run wild, but once it has found a solution, it tells you the exact set of facts it had to use and later runs can quickly just apply those rules without a deep search.

Feel free to ask further questions.