Program reasoning about own source code
I think you are asking about two different things. 


The ability of a programming language to represent all its programs as data. 
Reasoning about programs as data.


For analytical purposes it's useful to keep them apart. I will focus on the former.

The ability of a
programming languages to  represent, manipulate (and run) its programs
   as data  goes under terms such as meta-programming or
   homoiconicity. 

In an (awkward) way, all well-known programming languages can
   do meta-programming, namely by using the string data type together with the ability of invoking
   external programs (compiler, linker etc) on strings (e.g. by
   writing them to the file system first). However, that's probably not
   what you mean.  You probably have nice syntax in mind. Strings are not nice syntax for program representation because almost all strings don't represent programs, i.e. the string data type contains a lot of 'junk' when seen as a program representation mechanism. To make matters worse, the algebra of string operations has essentially no connection with the algebra of program construction.

What you probably have in mind is something much nicer. E.g. if $P$ is
a program, then  $\newcommand{\QUOTE}[1]{\langle #1\rangle}\QUOTE{P}$ is $P$, but
as data, at hand for manipulation and analysis. This is often called quotation. 
In practise, quotation is inflexible, so we use quasi-quotation instead, which
is a generalisation of quotation where the quote can have 'holes' in which programs can be run that provide data to 'fill' the holes. 
For example $$\newcommand{\SYNTAX}[1]{\mathsf{#1}}
\newcommand{\IF}[3]{\SYNTAX{if}\; #1 \; \SYNTAX{then}\; #2\; \SYNTAX{else}\; #3}\QUOTE{\IF{[\cdot]}{7}{8+9}}$$ is a quasi-quote representing a conditional where instead of a condition we have a hole $[\cdot]$. If the program $M$ evaluates to the data $\QUOTE{x &gt; 0}$, then the quasi-quote $$\QUOTE{\IF{[M]}{7}{8+9}}$$ evaluates to 
the data $$\QUOTE{\IF{x &gt; 0}{7}{8+9}}.$$

(Note that $M$ is a normal program (not a program as data) that returns a quoted program, i.e. program as data.)
In order for this to work, you need a data-type to represent programs. Typically that data-type is called AST (abstract syntax tree), and you can see (quasi-)quotes as abbreviation mechanisms for ASTs.

Several
programming languages offer quasi-quotes and other feature for meta-programming. It was Lisp with its
macroing functionality that pioneered this ability to treat programs as data.  Perhaps
unfortunately, the power of Lisp-based macros was long seen to rest
largely on Lisp’s minimalistic syntax; it was not until MetaML (1)
that a modern, syntactically rich language was shown to be capable of
meta-programming. Since then, MetaOCaml (2) (a descendant
of MetaML, important for its breakthrough in the still ongoing quest to solve the problem of how to type programs as data), Template Haskell (3)  and Converge (4) (the first language to get all key meta-programming features right in my opinion) have shown that a variety of modern programming languages can house
meta-programming. It is important to realise that we can take any programming
language $L$ and turn it into a meta-programming language $L_{mp}$
that is $L$ together with the ability of representing (and evaluating)
its own programs as data.

Representing the outcome of running program, given as data, is
achieved by adding an $\newcommand{\EVAL}{\mathsf{eval}}\EVAL(\cdot)$ function that takes a program (given as
data) as input and runs it, returning its result. E.g. if $P$ is a
program evaluating to 17 and $\QUOTE{P}$, the (quasi-)quoted version of $P$,
i.e. $P$ as data, then $\EVAL(\QUOTE{P})$ also returns 17. There are all
manner of subtleties here that I'm ignoring here such as the question when meta-programmed
programs are being evaluated (giving rise to the distinction between
compile-time and run-time meta-programmed), what to do with types or
failing evaluations, what happens to bound and free variables in the
process of going from $P$ to $\QUOTE{P}$ or vice versa. 

As to the second dimension, reasoning about programs given as data. As soon as you can convert programs into data, they are 'normal' data and can be reasoned about as data.  You can
use all manner of prover technology, e.g. dependent types or contracts
or interactive theorem provers or automated tools, as Joshua has
pointed out. However you will have to represent the semantics of your language in the reasoning process. If that language, as you require, have meta-programming abilities, things can become a bit tricky and not much work has been done in this direction, with (5) being the only program logic for this purpose. There is also Curry-Howard based work on reasoning about meta-programming (6, 7, 8). Note that these logic-based approaches, and the type-based approach (2) can indeed express properties that hold for all future meta-programming stages. Apart from (2) none of those papers have been implemented.

In summary: what you asked for has been implemented, but it's quite subtle, and there are still open questions, in particular to do with types and streamlined reasoning.




W. Taha. Multi-Stage Programming: Its Theory and Applications.
W. Taha and M. F. Nielsen. Environment classifiers.
T. Sheard and S. Peyton Jones. Template meta-programming for Haskell.
L. Tratt. Compile-time meta-programming in a dynamically typed OO language.
M. Berger, L. Tratt, Program Logics for Homogeneous Meta-Programming.
R. Davies, F. Pfenning, A modal analysis of staged computation.
R. Davies, A Temporal-Logic Approach to Binding-Time Analysis.
T. Tsukada, A. Igarashi. A logical foundation for environment classifiers.