patternModerate
Has Anyone Actually Created a System that Writes Computer Programs from specification?
Viewed 0 times
anyonespecificationwritescreatedsystemhasthatactuallycomputerprograms
Problem
Has anyone ever actually written a system (software or detailed explanation on paper with simple examples) that generates computer programs? I input $Prime(x) \wedge x<10$ and it creates a program that lists the prime numbers less than 10. $Prime(x)$ is simply defined as
$$1<x \wedge \not\exists A\; s.t. 1<A \wedge A<x \wedge x=A\times B,\mbox{ with }
A,B\in \mathbb{N}$$
Professors say they can but nobody gives actual complete examples.
$$1<x \wedge \not\exists A\; s.t. 1<A \wedge A<x \wedge x=A\times B,\mbox{ with }
A,B\in \mathbb{N}$$
Professors say they can but nobody gives actual complete examples.
Solution
This is a very active research topic, very promising, though full
automation of program generation probably has intrinsic limitations (but are human beings any better?).
But the idea is still be very useful in assisting considerably the
creation of programs by mechanizing many steps, and by automatically
checking the correctness of the program generation.
It is strongly related to a result in logic, called the Curry-Howard
correspondance (or isomorphism), that shows that computer programs and
mathematical proofs are very similar.
So the idea is that the system will take your program specification as a
theorem to be proved. In the case of your example, it would be
something like (informally): "there is a set of all prime numbers smaller
than 10".
Then, you will attempt to prove that theorem, and existing systems
will assist you in doing the proof, automating some parts, possibly the whole proof, and making
sure you never make errors.
From that proof one can then extract a program
that actually computes the wanted list of prime numbers that had been
initially specified.
Several systems were developed in the past to elucidate these ideas. One
of the better known was LCF by Robin Milner, who created the language
ML for that purpose. One of the currently most advanced systems is
Coq.
There are examples fully worked out, some of them quite complex. You may find some in the following article, though it is in no way simple reading and requires advanced knowledge of Logic.
automation of program generation probably has intrinsic limitations (but are human beings any better?).
But the idea is still be very useful in assisting considerably the
creation of programs by mechanizing many steps, and by automatically
checking the correctness of the program generation.
It is strongly related to a result in logic, called the Curry-Howard
correspondance (or isomorphism), that shows that computer programs and
mathematical proofs are very similar.
So the idea is that the system will take your program specification as a
theorem to be proved. In the case of your example, it would be
something like (informally): "there is a set of all prime numbers smaller
than 10".
Then, you will attempt to prove that theorem, and existing systems
will assist you in doing the proof, automating some parts, possibly the whole proof, and making
sure you never make errors.
From that proof one can then extract a program
that actually computes the wanted list of prime numbers that had been
initially specified.
Several systems were developed in the past to elucidate these ideas. One
of the better known was LCF by Robin Milner, who created the language
ML for that purpose. One of the currently most advanced systems is
Coq.
There are examples fully worked out, some of them quite complex. You may find some in the following article, though it is in no way simple reading and requires advanced knowledge of Logic.
Context
StackExchange Computer Science Q#22241, answer score: 11
Revisions (0)
No revisions yet.