Program reasoning about own source code The inspiration for this question is the following (vague) question: What are the programming language/logical foundations for having an AI which could reason about its own source code and modify it?

This isn't at all rigorous, so here is my attempt to extract a concrete question out of it. There are two things I'm interested in:

(A) A programming language P that can represent and manipulate its own programs as a datatype Program (e.g., as an AST). (If desired, a object of type Program can be converted into a String, which is the text of a valid program in that language. This would be the opposite of what a compiler does.)

(B) A method to reason about what a program in language P does. Here are two levels I'm thinking about it:


Another language Q (with theorem proving capabilities) which models what a P-program does. It should be able to express and prove statements like "the outcome of running Program p is foo."
A way to reason about what a program p:Program does in the language P itself. (So we are taking P=Q above.)


To what degree has something like this been implemented, or what is progress in this direction? What are the practical obstacles? In light of the original intention of the question, what is the best way to formalize the problem?

*

As the answers show (thanks!), both (A) and (B1) can be done separately, though it seems doing them together is more of a research question. 

Here were some of my first thoughts on the question (warning: rather vague). See also my comments on Martin Berger's answer.

I'm interested in the programming language modeling the same programming language, rather than a simpler one (so P=Q above). This would be a "proof of concept" of a program being able to "reason about its own source code." Dependently typed programming languages can give guarantees about the outputs of its functions, but this doesn't count as "reasoning about its own source code" any more than a "Hello world!" counts as a quine in a language that will automatically prints out a naked string---there needs to be some kind of quoting/self-reference. The analogue here is having a datatype representing Program.

It seems like a rather large project - the simpler the language, the harder it is to express everything within it; the more complicated the language, the more work has to be done to model the language.

In the spirit of the Recursion Theorem, a program can then "get" its own source code and modify it (i.e., output a modified version of itself). (B2) then tells us that the program should be able to express a guarantee about the modified program (this should be able to recurse, i.e., it should be able to express something about all future modifications-?).
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.