Can formal logic be a serious system implementation language?
It would be wonderful to have a language that realistically competes with C++, C# and Java for implementing industrial strength systems, which has a tractable semantics that supports formal verification of non-trivial programs, and a highly assured implementation guaranteeing that the semantics is correct. Alas, this is almost certainly impossible: any language with the sort of features found in existing industrial strength high-level languages is very unlikely to be capable of having either a tractable semantics or formally verified implementations. Some fairly widely used languages do have a formal semantics, notably the denotational semantics of Scheme and the celebrated formal operational semantics of ML, but these semantics do not provide a practical basis for formal reasoning about programs in the languages. They are, however, valuable as reference documents and for proving meta-theorems (like the type preservation for ML). There are subsets of real languages with tractable seman
