How do we start on computable contract theory?

I would go with the contract as a multi step decision tree.

In this tree, a contract condition is met when any or all of the listed conditions are met. If the condition is met, the contract drops to the next decision. We can see right away a simple graph semantic for contracts, something the Eth folks have already pioneered.

Both (and later, multiple) parties have their own decision trees. The trees convolve until they both reach a path end point.  The two general outcomes are completion or fails to deliver or timeout.

In the theory we look for probabilities of merit that can identify likelihood of passing a decision point.  Most of these probabilities derive from the distributions in the auto traded pits.  In the reverse direction, these decision trees hold hidden information, parties betting on certain conditional events.  That in turn requires shifts in pit balances, causing the revealed information to be priced. Decision trees are not bot traders, but they are like Watson from IBM, and belong in smart contracts.  Keep the boundary.

We end up with a kind of app language, like what they do with Ethereum, but no need of blockchain, all contracts run to completion.  The contract actions may include the return from the blockchain, registering ownership the most common action.

This is something doable in Javascript, a potential native language of secure element apps. We have that, isn't Solidify a Javascript?

A bit on theory:
The decision trees have a decomposition that preserves relative order.  For example, I can extract all the tx decisions from the tree, and recompose them in its own tree, maintaining order. Then convolve the tax tree, coincident with the other parties to the contract.  The extracted ta tree should step through without loops induced. We have a way to extract regulations and taxes as a separate tree.
nother are calls to bitcoin.  These can be extracted, and convolved against the conditions as they are encountered, thus making sure a chain of ownership is followed, independent of other contract conditions.