In mathematical logic, a formal system is a structure which includes, amongst other things, a set of axioms, and which is able to determine the truth or falsehood of statements with respect to those axioms.
A number of useful and counter-intuitive theorems were proved with respect to formal systems in the previous century. The Incompleteness Theorems are the most famous examples, but there are plenty of others.
I know that the connections between mathematical logic and computer science run very deep, but I have never been able to find a clear answer on what seems like a straightforward and important question: Can one think of a programming language as a formal system? Would this work for some languages but not other? In that case, what about the C programming language? Might it, perhaps, work only if we considered a subset of C or some other language?
If one could think of C or another language as a formal system, would applying well-known theorems about formal systems yield any interesting results?
Potential Examples of Axioms and Statements in C
C, like almost all programming languages, contains a form of arithmetic within itself. It contains the usual axioms that one learns at school with respect to the addition, subtraction and multiplication of integers. (Things get a little more interesting when we move to division and non-integers; C does not always return the expected result when dividing integers and working with floats.)
The rules of arithmetic provide the axioms. As for the statements, C includes the == operator, which we can use to test whether an asserted arithmetical equality is true, e.g. this minimal C program:
#include <stdio.h>
int main() {
if (2+2 == 4) {
printf("This is the expected result.\n");
} else {
printf("Something's gone badly wrong!\n");
}
return 0;
}
One could use a C program on the above lines to test whether each of a batch of arithmetical statements was true - or, for that matter, well-formed.