Your point on "slightly below" Turning machines caught my attention - exactly the same terminology I have used. I want as many proofs (assertions) as possible about code, and Rice's Theorem is a problem, so slightly below Turing is on the radar. If you are interested, we can discuss this. Shoot me an email at svembu at zoho ...