constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
In computer science, under imperative programming one understands a programming language-style in which a program largely consists of
a succession of commands (whence “imperative”)
for (in particular) accessing and modifying the global state of the computing environment
A typical example of imperative pseudocode would be of the form
n <- Read
n++
Write n
being the sequence of commands to, in this case:
read a (numerical) datum (from some input device) and store it in a global variable n
increment n
write the value of n
(to some output device).
Low-level languages are often imperative, reflecting the actual operation of the underlying computing machine; and medium-level imperative languages may be felt to have a transparent flow logic.
In its naive form the access and modification of global state variables means that imperative programs are hard to verify (since there is no guarantee that the global state is in the assumed form). This is generally in contrast to pure functional programming languages, which enforce that every procedure be a pure function in that its output and side-effect depends deterministically on its input (instead of also on the value of some global variables).
On the other hand, much of the features of imperative programs with access to a global state can be emulated/encapsulated in pure functional programming languages via the scheme of monadic data types (see there for more). With the syntactic sugar of do-notation [Launchbury 1993 §3.3] this allows purely functional languages to look essentially like imperative code while remaining verifiable.
See also:
The origin of do-notation for emulating imperative programming in functional programming languages via monadic data types:
Conversely, building features of functional programming languages into imperative languages:
Last revised on August 28, 2023 at 16:32:05. See the history of this page for a list of all contributions to it.