Are all possible programming languages a formal system?

Question

Based on the Wikipedia page for a formal system, will all programming languages be contained within the following rules?

• A finite set of of symbols.

(This seems obvious since the computer is a discrete machine with finite memory and therefore a finite number of ways to express a symbol.)

• A grammar.

• A set of axioms.

• A set of inference rules.

Are all possible languages constrained by these rules? Is there a notable proof?

EDIT:

I've been somewhat convinced that my question may actually be: can programming languages be represented by something other than a formal system?

Answer 1

Technically, yes, because you can make your formal system have a single axiom that says “the sequence of symbols is in the set $S$” where $S$ is the set of programs in the programming language. So this question isn't very meaningful. The notion of formal system is so general that it isn't terribly interesting in itself.

The point of using formal systems is to break down the definition of a language into easily-manageable parts. Formal systems lend themselves well to compositional definitions, where the meaning of a program is defined in terms of the meaning of its parts.

Note that your approach only defines whether a sequence of symbols is valid, but the definition of a programming language needs more than this: you also need to specify the meaning of each program. This can again be done by a formal system where the inference rules define a semantics for source programs.

Answer 2

The people doing programming language semantics try to describe programming languages in that way. Practicing programmers don't, their intuitive descriptions of the language is often fuzzy and outright contradictory (just take a look at the newbie questions and hurdles in your neighborhod freshman programming class, or at the problems people seek help with at stackoverflow). The programming languages in common use are much too complicated for a really complete formal description, so they don't qualify either. And then there are entertaining phenomena like undefined behaviour...

Answer 3

I would argue that an interpreter is, in fact, one way of defining a programming language. Since there are countably many Turing Machines, we could consider the set of all programming languages to be the set of all Turing Machines which take 2 inputs, a program and some input for that program, and output the result of "running" the program, with halting states to represent if the program was syntactically correct, encountered errors, etc.

Then, since a TM can be described by a finite set of symbols, a programming language can be described by a finite set of symbols.

Answer 4

Of course yes, and they have mostly been describe as is.

In fact most programming language has been define using Turing Machine which aren't formal system has you've define, but they are a kind of computation's model, define using formal language. Then grammar or axioms or complex inference rule (as expected for formal system) are not required.

Formal system can be view as a subset of Turing Machine with extra properties. Say differently you can have a programming language define using a Turing Machine as computation model but not fully fill the definition of formal system.

I'd like to add, inference rule required to define formal system are more than simple rule (as you can encounter in C for example or more simply in ASM), but we must ensure that any complex formulation of these rule can be decidable, it's mean, we must have inference's rule which rely on strong logical foundation.

Considering axiom, again we need more than a set of starting fact, sharing truth among the program, but we most ensure from a mathematical point of view that these axioms mixed with the inference rule provide us a computation framework which must be consistent (axioms mixed with inference rule should not lead the program to have an unexpected behavior or contradiction) and complete (no formula express using axiom and inference rule should be undecidable).

Most of time theses requirements aren't apply to the language itself but to it's type system in order to benefit of safety at compilation time by the mean of completeness and consistency, which as said earlier derive from inference rules and axiom (True by construction is you like).

To conclude, all programming language are formal language, in the way that the program itself is writing using a formal language, but they don't required to be formal system, contrary to mathematics's theory as number theory, abstract algebra, category theory which are express too by formal language but this time with the goal to form a formal system.

Which why Functional Programming matter.