> if your language is not Turing-complete, you could lock things down so that no crazy stuff happens, and prove that there is no way to bypass the security --assuming this problem is decidable, which can be the case if the language is not Turin-complete, but is hopeless otherwise.
It might be hopeless to try and "lock down" a Turing-complete language, but that's the wrong way to approach the problem. Rather than allowing undesired effects then trying to show they don't happen, simply avoid including them in the first place.
For example, consider an implementation of Conway's Game of Life, which takes in a text file describing the initial pattern (program), keeps running it until some stopping criterion is met (say, when the cell at position (0, 0) in the text file first becomes live), and outputs either the final state of the grid, or an error message (parse error, out of memory, etc.).
The Game of Life is Turing Complete[1], so it's undecidable in general whether a given text file will eventually produce a given pattern[2], including whether or not it will eventually trigger the stopping criterion. However, it's trivial to prove that our Game of Life implementation is secure against, say, shell execution attacks. How? We just need to prove that there are no patterns which cause shell execution. Since the Game of Life "language" has no concept of shell execution, our implementation doesn't need to expose anything which could allow it; it just needs to get and set booleans in an array, so this should be very straightforward to prove, even in a dangerous language like C. Just by verifying a single, known piece of code (our interpreter) we gain a security proof for all Game of Life programs.
Of course the Game of Life is a simplistic example, but this idea has been around for a while in functional programming, where it's common to solve a problem by first embedding a DSL (domain-specific language) inside our main or "host" language, then coding the solution in that DSL. This lets us, for example, write a parser using a DSL specifically tailored for parsing, or describe a diagram in a DSL specially tailored for drawing diagrams, etc.
We can prove all sorts of things about these DSLs, even if they're Turing Complete, by simply making them incapable of doing anything we don't want them to do. Since the "host" language (Lisp, Haskell, etc.) can already do potentially-dangerous things like accessing the filesystem, calling out to a shell, etc. there's no need to provide any of those features to the DSLs.
For example, if we want to parse the contents of an arbitrary file `F` using an arbitrary parsing program `P`, we can write a small piece of code in the host language for reading the contents of `F` as a string, then passing this string and `P` as arguments to the parsing DSL interpreter. This way, neither the parsing DSL or its interpreter need any access to the filesystem, so it can be straightforward to prove that no filesystem operations (e.g. accessing unauthorised data) can take place, regardless of what `F` and `P` are.
Likewise, if we want to render a diagram described by an arbitrary program `D` to an image file `I`, there's no need to provide filesystem access to the diagram DSL. Instead, we pass `D` to the diagram DSL interpreter and have it produce, say, an array of PNG data. The host language can then write this data to `I`, and again we can prove all kinds of properties like not overwriting a user's files, regardless of the program `D`.
Another nice benefit of using restricted DSLs like this is the ability to intercept all effects which we do provide to the language. For example, just because we provide `read(path)` and `write(path, string)` primitive to our DSL, doesn't mean that such programs can access the filesystem. We might choose to have an interpreter which implements these by reading and writing files, but we can just as well write an interpreter which loads and stores strings in a hash table. This is useful for testing, debugging, tracing, etc.
[1] http://rendell-attic.org/gol/utm/index.htm
[2] This only holds "in general"; there are particular patterns which are decidable, known as "Garden of Eden" patterns; these cannot exist after the first time step, so we just need to check whether they appear as-is in the initial program https://en.wikipedia.org/wiki/Garden_of_Eden_(cellular_autom...