<p>No there is no current system that does all four steps in your system. If you want to design a system one of the first requirements is homoiconic language. At minimum you would want your core programming language that you have as small as possible so that when you enter the system and start to make it interpret itself it will work. So therefore you want a metacircular interpreter which was pioneered in lisp. Other languages have done it also but there is a enormous amount of existing research on lisp.</p>

<p>The first step if you want to do this is to have a homoiconic language like Lisp or some framework where you can reason about a running program. Lisp is used for this for the sole reason that you could define a metacircular interpreter in the language or you can just treat your code as data. Treating the code as data is the most important thing. <a href="http://c2.com/cgi/wiki?HomoiconicLanguages">There is along discussion about what homoiconic means on c2 wiki.</a></p>

<p>For example in Lisp your "Program" datatype is valid lisp programs. You pass the lisp programs to an interpreter and it computes something. It gets rejected by the interpreter if you don't program a valid "Program". </p>

<p>Therefore a homoiconic language does three of your requirements. You can even in lisp define the idea of a formal program.</p>

<p>Can you model lisp inside lisp? Yes this is frequently done mainly as an exercise at the end of a lisp programming book to test your abilities. <a href="https://mitpress.mit.edu/sicp/full-text/book/book.html">SICP</a></p>

<p>At the current time issue four is a research question and below is what I have found that attempts to answer this question.</p>

<p>I would say there are many types of programs that attempt to do this. Below is all of the programs that I know about.</p>

<ul>
<li><p><a href="http://www.jslint.com/">JSLint</a> is an example of a static analyzers that take machine code or some other language and look for bugs explicitly. Then it asks for a programmer to correct that.</p></li>
<li><p><a href="https://coq.inria.fr/">Coq</a> is a environment that allows you to specify proofs using a programming language. It also has tactics where it suggests ways for you to solve the problem. Still this expects a human to do the work. Coq uses dependant types to work and is therefore very type theoretic. It is very popular among computer scientists and people working on Homotopy Type Theory.</p></li>
<li><p><a href="https://www.cs.utexas.edu/users/moore/acl2/">ACL2</a> on the other hand is an automated theorem prover. This system will prove statements based on something that you program.</p></li>
<li><p>ACL2 and Coq have a software plugin that interface their system with a <a href="http://staff.computing.dundee.ac.uk/jheras/acl2ml/">machine learning system</a>.  What is used to train these systems are previously written programs. From my understanding these systems add another feature where you have not only your tactics but suggested theorems that aid in proof development.</p></li>
</ul>

<p>Below is more of a foundational of what your question means.</p>

<ul>
<li><a href="https://gcc.gnu.org/onlinedocs/gcc/Optimize-Options.html">gcc</a> is an example of an optimizng compiler which can take itself as input and then output an optimized version of itself. The idea of a compiler that translates programs from one representation to another and improves the speed due to some optimization flag is very well understood. Once you bootstrap the compiler and it generates valid machine code then you can add an optimization and recompile the compiler and it makes a more efficient version of itself.</li>
</ul>

CC BY-SA 3.0
2015-09-04T19:17:10.190Z
There is no need to make the language as minimal as possible. You can add the relevant meta-programming features to any language. Taha's MetaML work has shown this. Indeed the addition of meta-programming capabilities is mechanical.
Martin Berger
CC BY-SA 3.0
2015-09-04T19:18:34.063Z
I also disagree that "no current system that does all four steps". Question 4 only talks about running programs given as code. That's perfectly possible, indeed even Javascript's eval does it.
Martin Berger
CC BY-SA 3.0
2015-09-04T19:19:59.893Z
@MartinBerger what I mean is you make the core kernel as minimal as possible . Also if you even begin to want to hope that your system will do #4 you will want a system that you can train not just humans but computers to use so it would benefit you to have a minimal system and they have libraries that are coded in that system like a meta programming template
Joshua Herman
CC BY-SA 3.0
2015-09-04T19:34:26.383Z
It depends on what (4) we are talking about. The original question contains two elaborations of those. The first is trivial, you just run the program. The second one can be handled by the logic I cited as (5) in my answer of the typing system (2). The later is implemented in MetaOCaml. But there is scope for more research: neither (2) nor (5) can deal with arbitrary forms of meta-programming, and the properties guarantedd by (2) are a bit weak (after all, it's a typing system with type inference).
Martin Berger
CC BY-SA 3.0
2015-09-04T19:36:37.447Z
As to "you make the core kernel as minimal as possible": that's not required. You can add full meta-programming to any language.
Martin Berger
CC BY-SA 3.0
2015-09-05T22:18:35.820Z
@MartinBerger you should incorporate the things you don't agree with into my answer so that you get the check mark. This question is too vague at this point .
Joshua Herman
CC BY-SA 3.0
2015-09-06T17:42:52.337Z
Don't worry about it. The original question has evolved quite a bit.
Martin Berger
CC BY-SA 3.0
2015-09-04T15:26:59.247Z
2015-09-04T18:50:43.673Z
2015-09-04T18:50:43.673Z
Joshua Herman
<p>As <a href="https://cstheory.stackexchange.com/a/32471/21598">@user217281728's answer</a> mentions there are a type of machines related more to inference and AI, called <a href="https://en.wikipedia.org/wiki/G%C3%B6del_machine" rel="nofollow noreferrer">Gödel Machines</a></p>

<blockquote>
  <p>A Gödel machine is a self-improving computer program invented by
  Jürgen Schmidhuber that solves problems in an optimal way. It uses a
  recursive self-improvement protocol in which it rewrites its own code
  when it can prove the new code provides a more optimal strategy.
  The machine was invented by Jürgen Schmidhuber, but is named after
  Kurt Gödel who inspired the mathematical theories.</p>
</blockquote>

<p>The referenced publication of Jürgen Schmidhuber on <a href="http://arxiv.org/abs/cs/0309048v5" rel="nofollow noreferrer">"Goedel Machines: Self-Referential Universal Problem Solvers Making Provably Optimal Self-Improvements", (2006) arXiv:cs/0309048v5</a></p>

<p>The way the machine works to implement <em>meta-learning</em> has two phases:</p>

<ol>
<li>Learning from data (level 1, learn)</li>
<li>Using learned data to modify/optimise its source code/algorithm (level 2, learn to learn)</li>
</ol>

<p>Since the machine modifies its own source it is self-referential, i.e has the self-modification property (see also <a href="https://cs.stackexchange.com/a/29646/17369">here</a>).</p>

<p>In this sense it can modify the learning algorithm itself in a rigorous sense (proving optimal self-modifications). There are the problems with self-reference and undecidability which in this case take the form:</p>

<blockquote>
  <p>..a Gödel machine with unlimited computational resources must ignore
  those self-improvements whose effectiveness it cannot prove</p>
</blockquote>

<p>Other languages (and their associated interpreter machines) which have the self-modification property are for example <a href="https://en.wikipedia.org/wiki/Lisp_%28programming_language%29" rel="nofollow noreferrer">LISP</a>.</p>

<p>In LISP code and data are inter-changeable, or the source code AST is available as data, in the LISP program and can be modified as data. On the other hand, data can be seen as AST, for some source code.</p>

<p><strong>update</strong></p>

<p>There are <a href="https://www.eecis.udel.edu/~case/self-ref.html" rel="nofollow noreferrer">other machines as well</a>, like <a href="http://www.self-programming-machines.org/" rel="nofollow noreferrer">self-programming machines</a> (among others) which combine <strong>self-reference</strong>, <strong>self-reproduction</strong> and <strong>self-programming</strong>.</p>

<p>One interesting aspect of the above is that <strong>self-reference is not problematic</strong> at all, rather it is a <strong>necessary element in <a href="https://en.wikipedia.org/wiki/Von_Neumann_universal_constructor" rel="nofollow noreferrer">self-reproduction</a> / self-programming automata</strong>.</p>

<p>For further details (and more publications) refer to <a href="http://www.self-programming-machines.org/pdf/SPM3.pdf" rel="nofollow noreferrer">J.P Moulin, C.R Biologies 329 (2006)</a></p>

<p><strong>abstract</strong></p>

<blockquote>
  <p>Living systems are capable to have appropriate responses to
  unpredictable environment. This kind of self-organisation seems to
  operate as a self-programming machine, i.e an oprganisation able to
  modify itself. Until now the models of self-organisation of living
  beings proposed are functions solutions of differential systems or
  transition functions of automata. These functions are fixed and these
  models are therefore unable to modify their organisation. On the other
  hand, computer science propose a lot of models having the properties
  of adaptive systems of living beings, but all these models depend on
  the comparison between a goal and the results and ingenious choices of
  parameters by programmers, whereas there are no programmer's intention
  nor choice in the living systems. From two best known examples of
  adaptive systems of living beings, nervous system and immune system
  that have in common that the external signals modify the rewriting of
  their organisation and therefore works as a self-organising machines,
  we devised machines with a finite set of inputs, based upon a
  recurrence, are able to rewrite their organisation (Self-programming
  machines or $\mathbb{m}_\mathbb{sp}$) whenever external conditions
  vary and have striking properties of adaptation.
  $\mathbb{M}_\mathbb{sp}$ have similar properties whatever the
  operation defining the recurrence maybe. These results bring us to
  make the following statement: adaptive properties of living systems
  can be explained by their ability to rewrite their organisation
  whenever external conditions vary under the only assumption that the
  rewriting mechanism be a deterministic constant recurrence in a finite
  state set.</p>
</blockquote>

CC BY-SA 3.0
2015-09-07T21:20:31.290Z
2016-01-17T14:38:26.030Z
2017-04-13T12:48:30.830Z
Nikos M.
<p>This paper by Jurgen Schmidthuber might be of interest:</p>

<p><a href="http://arxiv.org/pdf/cs/0309048.pdf" rel="nofollow">http://arxiv.org/pdf/cs/0309048.pdf</a></p>

CC BY-SA 3.0
2016-01-22T05:09:52.147Z
plz give a summary at least
vzn
CC BY-SA 3.0
2015-09-07T19:12:10.323Z
2015-09-07T19:12:10.323Z
NietzscheanAI
<p>I think you are asking about two different things. </p>

<ul>
<li>The ability of a programming language to represent all its programs as data. </li>
<li>Reasoning about programs as data.</li>
</ul>

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

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

<p>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.</p>

<p>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 <strong>quotation</strong>. 
In practise, quotation is inflexible, so we use <strong>quasi-quotation</strong> 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}}.$$</p>

<p>(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.</p>

<p>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 <strong>any</strong> 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.</p>

<p>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 <em>when</em> 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. </p>

<p>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.</p>

<p>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.</p>

<hr>

<ol>
<li><p>W. Taha. <a href="http://www.cs.rice.edu/~taha/publications/thesis/thesis.pdf">Multi-Stage Programming: Its Theory and Applications</a>.</p></li>
<li><p>W. Taha and M. F. Nielsen. <a href="http://www.cs.rice.edu/~taha/publications/conference/popl03.pdf">Environment classifiers</a>.</p></li>
<li><p>T. Sheard and S. Peyton Jones. <a href="http://research.microsoft.com/pubs/67015/meta-haskell.pdf">Template meta-programming for Haskell</a>.</p></li>
<li><p>L. Tratt. <a href="http://tratt.net/laurie/research/pubs/papers/tratt__compile-time_meta-programming_in_a_dynamically_typed_oo_language.pdf">Compile-time meta-programming in a dynamically typed OO language</a>.</p></li>
<li><p>M. Berger, L. Tratt, <a href="http://users.sussex.ac.uk/~mfb21/publications/lpar10/">Program Logics for Homogeneous Meta-Programming</a>.</p></li>
<li><p>R. Davies, F. Pfenning, <a href="https://www.cs.cmu.edu/~fp/papers/jacm00.pdf">A modal analysis of staged computation</a>.</p></li>
<li><p>R. Davies, <a href="http://www.brics.dk/RS/95/51/BRICS-RS-95-51.pdf">A Temporal-Logic Approach to Binding-Time Analysis</a>.</p></li>
<li><p>T. Tsukada, A. Igarashi. <a href="http://www.fos.kuis.kyoto-u.ac.jp/~igarashi/papers/classifiers.html">A logical foundation for environment classifiers</a>.</p></li>
</ol>

CC BY-SA 3.0
2015-09-04T20:43:14.270Z
You're right - the programming language P can be different from the language Q that expresses theorems/proofs about programs in that language (which can be in Coq for instance). The kind of theorem that I'm thinking about goes like this: Suppose we have a carefully designed program A_1.
Thm: For every n the following holds: Program A_n will output (m_n, A_{n+1}), where m_n is an integer, A_{n+1} is another program (e.g., obtained by modifying A_n in some way), and for all n, we have that m_n>0.
Holden Lee
CC BY-SA 3.0
2015-09-04T20:43:32.970Z
(The science fiction version of this is that we have a "proof" that a program that keeps modifying itself, will never press the button that launches a nuclear missile, say, or that the program will always optimize a certain quantity.)
Holden Lee
CC BY-SA 3.0
2015-09-04T20:43:39.133Z
This is why I wanted to make a distinction between running the program, and reasoning on what the program will output - we want to know properties of what it will do before it's run, without running it. Note that if we want A_n to be able to "modify its source code" to produce A_{n+1}, then P will necessarily have metaprogramming abilities (which puts us in the position of (5)).
Holden Lee
CC BY-SA 3.0
2015-09-04T20:43:51.180Z
It still seems to me that it would be interesting for P=Q. Hypothetically, A is an AI program and the way that would modify itself is by reasoning about its own code - for example, write down theorems about bits of code, proving them, and only then modifying its code. Then it seems P would need to have the capabilities of Q.
Holden Lee
CC BY-SA 3.0
2015-09-04T20:48:47.373Z
@HoldenLee It's possible to write programs like A_n. If you use strings as representative of programs, this can be done trivially in any language, if you want quasi-quotes or similar, this is possible in e.g. Converge. I don't understand the role of m_n in the construction.
Martin Berger
CC BY-SA 3.0
2015-09-04T20:51:51.643Z
@HoldenLee As to "we want to know properties of what it will do before it's run, without running it", this is impossible (AI or not) in general by [Rice's theorem](https://en.wikipedia.org/wiki/Rice%27s_theorem), a straightforward consequence of the halting problem. Of course when you are constructing a new program by modification of an old one, you can simply keep evolving the relevant correctness proof along with the program.
Martin Berger
CC BY-SA 3.0
2015-09-04T21:04:31.147Z
The m_n is just a stand-in for any properties or outputs of program A_n. I just wanted to make a point that Q has to model the metaprogramming capabilities of P in order to express and prove statements like: in the sequence of modified programs A_n, some property will always remain true (e.g., A_n will always spit out a program that sorts a list).

I'm not saying that for every A there will exist a proof - but for *some* A's there will exist one (we get to write the program A_1), and for those programs we can express it in language Q.
Holden Lee
CC BY-SA 3.0
2015-09-04T21:14:28.307Z
@HoldenLee OK, I see. Most languages don't offer the ability to express much in the way of program properties. MetaOcaml's typing system guarantees properties for all future states of generated code, but being a typing system allowing type-inference, the properties that could be expressed this way must be weak. However, there is nothing preventing you from adding MP features to languages with the ability to express rich properties, e.g. Agda: you generate a new program and before outputting it, you type-check against the target type.
Martin Berger
CC BY-SA 3.0
2015-09-04T17:38:36.657Z
2015-09-04T20:46:01.933Z
2015-09-04T20:46:01.933Z
Martin Berger
<p>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?</p>

<p>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:</p>

<p>(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.)</p>

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

<ol>
<li>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."</li>
<li>A way to reason about what a program p:Program does <em>in the language P itself.</em> (So we are taking P=Q above.)</li>
</ol>

<p>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?</p>

<p>*</p>

<p>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. </p>

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

<p>I'm interested in the programming language modeling <em>the same</em> 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.</p>

<p>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.</p>

<p>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 <em>should be able to express a guarantee about the modified program</em> (this should be able to recurse, i.e., it should be able to express something about all future modifications-?).</p>

CC BY-SA 3.0
2015-09-04T19:11:43.027Z
Why do you need the language to act as a theorem prover to establish that "the outcome of running Program p is foo"? The language could simply run p! Indeed, that's what's happening.
Martin Berger
CC BY-SA 3.0
2015-09-04T20:24:03.313Z
https://en.wikipedia.org/wiki/Reflection_(computer_programming)
Kaveh
CC BY-SA 3.0
2015-09-04T20:35:08.013Z
Note that in principle all language which can implement an interpreter for themselves can do things you are requiring. In a more mathematical way, the recursion theorem holds for any strong enough model of computation. Some programming languages just make it easier by having it built in. Same for reasoning: you can implement any reasoning system inside these languages. Of course one cannot expect to reason everything, e.g. the halting problem for the programs.
Kaveh
CC BY-SA 3.0
2015-09-04T20:36:56.070Z
I think the question is not very clear. You should have a look at the programming languages like Python, Java, and those mentioned by Martin in his answer and clarify the question so either it is clear that they meet what you are looking for or if not why not.
Kaveh
CC BY-SA 3.0
2015-09-04T21:33:33.243Z
Edited - let me know if this is better.
Holden Lee
CC BY-SA 3.0
2015-09-05T06:04:40.560Z
@HoldenLee As to "P=Q", the established terminology is "homogeneous meta-programming", which is opposed to "heterogeneous meta-programming" where P $\neq$ Q.
Martin Berger
CC BY-SA 3.0
2015-09-05T22:15:55.550Z
@MartinBerger can you merge my statements into yours so you can get the answer credit? At this point neither of us would and the person that is asking the question would not give anything a check mark. Either that or the question is too vague.
Joshua Herman
CC BY-SA 3.0
2015-09-06T01:39:09.643Z
I'll check an answer in a few days (it's my habit to wait a bit to give everyone who wants to a chance to chime in).
Holden Lee
CC BY-SA 3.0
2016-01-17T14:26:55.213Z
see my updated answer with references to self-programming machines/automata which relate to the later part of your question
Nikos M.
CC BY-SA 3.0
2016-01-20T17:43:34.213Z
there is some connection to genetic algorithms/ genetic programming etc
vzn
CC BY-SA 3.0
2016-01-22T05:08:56.560Z
this also reminds me of [AGI](https://en.wikipedia.org/wiki/Artificial_general_intelligence) because there is some anthropomorphism of a presumably intelligent entity "reasoning" & there is some near-discussion in that literature
vzn
<pl.programming-languages><ai.artificial-intel><recursion>
Program reasoning about own source code
Holden Lee
# Program reasoning about own source code

(Asked by: username_0 on 2015-09-04)

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:

1. 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."
2. 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-?).

**Tags:** pl.programming-languages, ai.artificial-intel, recursion
> **Comments:**
> **username_1**: Why do you need the language to act as a theorem prover to establish that "the outcome of running Program p is foo"? The language could simply run p! Indeed, that's what's happening.  
> **username_2**: https://en.wikipedia.org/wiki/Reflection_(computer_programming)  
> **username_2**: Note that in principle all language which can implement an interpreter for themselves can do things you are requiring. In a more mathematical way, the recursion theorem holds for any strong enough model of computation. Some programming languages just make it easier by having it built in. Same for reasoning: you can implement any reasoning system inside these languages. Of course one cannot expect to reason everything, e.g. the halting problem for the programs.  
> **username_2**: I think the question is not very clear. You should have a look at the programming languages like Python, Java, and those mentioned by Martin in his answer and clarify the question so either it is clear that they meet what you are looking for or if not why not.  
> **username_0**: Edited - let me know if this is better.  
> **username_1**: @HoldenLee As to "P=Q", the established terminology is "homogeneous meta-programming", which is opposed to "heterogeneous meta-programming" where P $\neq$ Q.  
> **username_3**: @MartinBerger can you merge my statements into yours so you can get the answer credit? At this point neither of us would and the person that is asking the question would not give anything a check mark. Either that or the question is too vague.  
> **username_0**: I'll check an answer in a few days (it's my habit to wait a bit to give everyone who wants to a chance to chime in).  
> **username_4**: see my updated answer with references to self-programming machines/automata which relate to the later part of your question  
> **username_5**: there is some connection to genetic algorithms/ genetic programming etc  
> **username_5**: this also reminds me of [AGI](https://en.wikipedia.org/wiki/Artificial_general_intelligence) because there is some anthropomorphism of a presumably intelligent entity "reasoning" & there is some near-discussion in that literature  

---

## 4 answers

### Answer by username_1 on 2015-09-04. Score: 15 | Accepted answer

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 > 0}$, then the quasi-quote $$\QUOTE{\IF{[M]}{7}{8+9}}$$ evaluates to
the data $$\QUOTE{\IF{x > 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.

---

1. W. Taha. [Multi-Stage Programming: Its Theory and Applications](http://www.cs.rice.edu/~taha/publications/thesis/thesis.pdf).
2. W. Taha and M. F. Nielsen. [Environment classifiers](http://www.cs.rice.edu/~taha/publications/conference/popl03.pdf).
3. T. Sheard and S. Peyton Jones. [Template meta-programming for Haskell](http://research.microsoft.com/pubs/67015/meta-haskell.pdf).
4. L. Tratt. [Compile-time meta-programming in a dynamically typed OO language](http://tratt.net/laurie/research/pubs/papers/tratt__compile-time_meta-programming_in_a_dynamically_typed_oo_language.pdf).
5. M. Berger, L. Tratt, [Program Logics for Homogeneous Meta-Programming](http://users.sussex.ac.uk/~mfb21/publications/lpar10/).
6. R. Davies, F. Pfenning, [A modal analysis of staged computation](https://www.cs.cmu.edu/~fp/papers/jacm00.pdf).
7. R. Davies, [A Temporal-Logic Approach to Binding-Time Analysis](http://www.brics.dk/RS/95/51/BRICS-RS-95-51.pdf).
8. T. Tsukada, A. Igarashi. [A logical foundation for environment classifiers](http://www.fos.kuis.kyoto-u.ac.jp/~igarashi/papers/classifiers.html).

> **Comments:**
> **username_0**: You're right - the programming language P can be different from the language Q that expresses theorems/proofs about programs in that language (which can be in Coq for instance). The kind of theorem that I'm thinking about goes like this: Suppose we have a carefully designed program A_1. Thm: For every n the following holds: Program A_n will output (m_n, A_{n+1}), where m_n is an integer, A_{n+1} is another program (e.g., obtained by modifying A_n in some way), and for all n, we have that m_n>0.  
> **username_0**: (The science fiction version of this is that we have a "proof" that a program that keeps modifying itself, will never press the button that launches a nuclear missile, say, or that the program will always optimize a certain quantity.)  
> **username_0**: This is why I wanted to make a distinction between running the program, and reasoning on what the program will output - we want to know properties of what it will do before it's run, without running it. Note that if we want A_n to be able to "modify its source code" to produce A_{n+1}, then P will necessarily have metaprogramming abilities (which puts us in the position of (5)).  
> **username_0**: It still seems to me that it would be interesting for P=Q. Hypothetically, A is an AI program and the way that would modify itself is by reasoning about its own code - for example, write down theorems about bits of code, proving them, and only then modifying its code. Then it seems P would need to have the capabilities of Q.  
> **username_1**: @HoldenLee It's possible to write programs like A_n. If you use strings as representative of programs, this can be done trivially in any language, if you want quasi-quotes or similar, this is possible in e.g. Converge. I don't understand the role of m_n in the construction.  
> **username_1**: @HoldenLee As to "we want to know properties of what it will do before it's run, without running it", this is impossible (AI or not) in general by [Rice's theorem](https://en.wikipedia.org/wiki/Rice%27s_theorem), a straightforward consequence of the halting problem. Of course when you are constructing a new program by modification of an old one, you can simply keep evolving the relevant correctness proof along with the program.  
> **username_0**: The m_n is just a stand-in for any properties or outputs of program A_n. I just wanted to make a point that Q has to model the metaprogramming capabilities of P in order to express and prove statements like: in the sequence of modified programs A_n, some property will always remain true (e.g., A_n will always spit out a program that sorts a list).  I'm not saying that for every A there will exist a proof - but for *some* A's there will exist one (we get to write the program A_1), and for those programs we can express it in language Q.  
> **username_1**: @HoldenLee OK, I see. Most languages don't offer the ability to express much in the way of program properties. MetaOcaml's typing system guarantees properties for all future states of generated code, but being a typing system allowing type-inference, the properties that could be expressed this way must be weak. However, there is nothing preventing you from adding MP features to languages with the ability to express rich properties, e.g. Agda: you generate a new program and before outputting it, you type-check against the target type.  

---

### Answer by username_3 on 2015-09-04. Score: 6

No there is no current system that does all four steps in your system. If you want to design a system one of the first requirements is homoiconic language. At minimum you would want your core programming language that you have as small as possible so that when you enter the system and start to make it interpret itself it will work. So therefore you want a metacircular interpreter which was pioneered in lisp. Other languages have done it also but there is a enormous amount of existing research on lisp.

The first step if you want to do this is to have a homoiconic language like Lisp or some framework where you can reason about a running program. Lisp is used for this for the sole reason that you could define a metacircular interpreter in the language or you can just treat your code as data. Treating the code as data is the most important thing. [There is along discussion about what homoiconic means on c2 wiki.](http://c2.com/cgi/wiki?HomoiconicLanguages)

For example in Lisp your "Program" datatype is valid lisp programs. You pass the lisp programs to an interpreter and it computes something. It gets rejected by the interpreter if you don't program a valid "Program".

Therefore a homoiconic language does three of your requirements. You can even in lisp define the idea of a formal program.

Can you model lisp inside lisp? Yes this is frequently done mainly as an exercise at the end of a lisp programming book to test your abilities. [SICP](https://mitpress.mit.edu/sicp/full-text/book/book.html)

At the current time issue four is a research question and below is what I have found that attempts to answer this question.

I would say there are many types of programs that attempt to do this. Below is all of the programs that I know about.

* [JSLint](http://www.jslint.com/) is an example of a static analyzers that take machine code or some other language and look for bugs explicitly. Then it asks for a programmer to correct that.
* [Coq](https://coq.inria.fr/) is a environment that allows you to specify proofs using a programming language. It also has tactics where it suggests ways for you to solve the problem. Still this expects a human to do the work. Coq uses dependant types to work and is therefore very type theoretic. It is very popular among computer scientists and people working on Homotopy Type Theory.
* [ACL2](https://www.cs.utexas.edu/users/moore/acl2/) on the other hand is an automated theorem prover. This system will prove statements based on something that you program.
* ACL2 and Coq have a software plugin that interface their system with a [machine learning system](http://staff.computing.dundee.ac.uk/jheras/acl2ml/). What is used to train these systems are previously written programs. From my understanding these systems add another feature where you have not only your tactics but suggested theorems that aid in proof development.

Below is more of a foundational of what your question means.

* [gcc](https://gcc.gnu.org/onlinedocs/gcc/Optimize-Options.html) is an example of an optimizng compiler which can take itself as input and then output an optimized version of itself. The idea of a compiler that translates programs from one representation to another and improves the speed due to some optimization flag is very well understood. Once you bootstrap the compiler and it generates valid machine code then you can add an optimization and recompile the compiler and it makes a more efficient version of itself.

> **Comments:**
> **username_1**: There is no need to make the language as minimal as possible. You can add the relevant meta-programming features to any language. Taha's MetaML work has shown this. Indeed the addition of meta-programming capabilities is mechanical.  
> **username_1**: I also disagree that "no current system that does all four steps". Question 4 only talks about running programs given as code. That's perfectly possible, indeed even Javascript's eval does it.  
> **username_3**: @MartinBerger what I mean is you make the core kernel as minimal as possible . Also if you even begin to want to hope that your system will do #4 you will want a system that you can train not just humans but computers to use so it would benefit you to have a minimal system and they have libraries that are coded in that system like a meta programming template  
> **username_1**: It depends on what (4) we are talking about. The original question contains two elaborations of those. The first is trivial, you just run the program. The second one can be handled by the logic I cited as (5) in my answer of the typing system (2). The later is implemented in MetaOCaml. But there is scope for more research: neither (2) nor (5) can deal with arbitrary forms of meta-programming, and the properties guarantedd by (2) are a bit weak (after all, it's a typing system with type inference).  
> **username_1**: As to "you make the core kernel as minimal as possible": that's not required. You can add full meta-programming to any language.  
> **username_3**: @MartinBerger you should incorporate the things you don't agree with into my answer so that you get the check mark. This question is too vague at this point .  
> **username_1**: Don't worry about it. The original question has evolved quite a bit.  

---

### Answer by username_4 on 2015-09-07. Score: 5

As [@user217281728's answer](https://cstheory.stackexchange.com/a/32471/21598) mentions there are a type of machines related more to inference and AI, called [Gödel Machines](https://en.wikipedia.org/wiki/G%C3%B6del_machine)

> A Gödel machine is a self-improving computer program invented by
> Jürgen Schmidhuber that solves problems in an optimal way. It uses a
> recursive self-improvement protocol in which it rewrites its own code
> when it can prove the new code provides a more optimal strategy.
> The machine was invented by Jürgen Schmidhuber, but is named after
> Kurt Gödel who inspired the mathematical theories.

The referenced publication of Jürgen Schmidhuber on ["Goedel Machines: Self-Referential Universal Problem Solvers Making Provably Optimal Self-Improvements", (2006) arXiv:cs/0309048v5](http://arxiv.org/abs/cs/0309048v5)

The way the machine works to implement *meta-learning* has two phases:

1. Learning from data (level 1, learn)
2. Using learned data to modify/optimise its source code/algorithm (level 2, learn to learn)

Since the machine modifies its own source it is self-referential, i.e has the self-modification property (see also [here](https://cs.stackexchange.com/a/29646/17369)).

In this sense it can modify the learning algorithm itself in a rigorous sense (proving optimal self-modifications). There are the problems with self-reference and undecidability which in this case take the form:

> ..a Gödel machine with unlimited computational resources must ignore
> those self-improvements whose effectiveness it cannot prove

Other languages (and their associated interpreter machines) which have the self-modification property are for example [LISP](https://en.wikipedia.org/wiki/Lisp_%28programming_language%29).

In LISP code and data are inter-changeable, or the source code AST is available as data, in the LISP program and can be modified as data. On the other hand, data can be seen as AST, for some source code.

**update**

There are [other machines as well](https://www.eecis.udel.edu/~case/self-ref.html), like [self-programming machines](http://www.self-programming-machines.org/) (among others) which combine **self-reference**, **self-reproduction** and **self-programming**.

One interesting aspect of the above is that **self-reference is not problematic** at all, rather it is a **necessary element in [self-reproduction](https://en.wikipedia.org/wiki/Von_Neumann_universal_constructor) / self-programming automata**.

For further details (and more publications) refer to [J.P Moulin, C.R Biologies 329 (2006)](http://www.self-programming-machines.org/pdf/SPM3.pdf)

**abstract**

> Living systems are capable to have appropriate responses to
> unpredictable environment. This kind of self-organisation seems to
> operate as a self-programming machine, i.e an oprganisation able to
> modify itself. Until now the models of self-organisation of living
> beings proposed are functions solutions of differential systems or
> transition functions of automata. These functions are fixed and these
> models are therefore unable to modify their organisation. On the other
> hand, computer science propose a lot of models having the properties
> of adaptive systems of living beings, but all these models depend on
> the comparison between a goal and the results and ingenious choices of
> parameters by programmers, whereas there are no programmer's intention
> nor choice in the living systems. From two best known examples of
> adaptive systems of living beings, nervous system and immune system
> that have in common that the external signals modify the rewriting of
> their organisation and therefore works as a self-organising machines,
> we devised machines with a finite set of inputs, based upon a
> recurrence, are able to rewrite their organisation (Self-programming
> machines or $\mathbb{m}\_\mathbb{sp}$) whenever external conditions
> vary and have striking properties of adaptation.
> $\mathbb{M}\_\mathbb{sp}$ have similar properties whatever the
> operation defining the recurrence maybe. These results bring us to
> make the following statement: adaptive properties of living systems
> can be explained by their ability to rewrite their organisation
> whenever external conditions vary under the only assumption that the
> rewriting mechanism be a deterministic constant recurrence in a finite
> state set.


---

### Answer by username_6 on 2015-09-07. Score: 3

This paper by Jurgen Schmidthuber might be of interest:

<http://arxiv.org/pdf/cs/0309048.pdf>

> **Comments:**
> **username_5**: plz give a summary at least  

---

