Have a look at the ProCos work from Tony Hoare in the early 90s. I cannot remember the precise details but the language mixed contracts with statements in a clear algebraic fashion, and was compiled by bootstrapping.

Matthew: many thanks to your asking for clarification and I should have been more clear about the verification I meant. I did mean the verification that is at the such as a level that would more or less eliminate the software testing that cost too many efforts for both academia and industry today. For example, by running the compiled code with certain test inputs, the program will either output the correct results, or report the errors in the code. I know this is quite challenging and a lot of intellectuals have thought about this possibility very early on, otherwise they would not continue to put efforts on doing all sorts of things related to software verification, model check, formal or program-analysis based quality assurance, etc. I am just a late thinker about this possibility.

Assertions are the closest you'll find with current programming languages -essentially "make or break" statements that you scatter along your code, and completely abort execution if any test condition goes wrong. But you must know what those test conditions should be, which is an art in itself. But eliminating testing...sorry, no can do. It would be like eliminating formal proof from mathematics, with the added catch that an algorithm may be formally correct, but any given implementaiton of it is not guaranteed to be so. Proving that a program is 100% correct for all possible inputs is reconducible to a special case of the Halting Problem, which is demonstrated to be unsolvable ever since 1936 by Alan Turing: it cannot be done except in very trivial cases and/or with very restrictive assumptions on the set of possible inputs and the complexity of the employed algorithms.

Yes, I agree that the sort of verification you are looking for is program proof. I have recently attended a very interesting presentation for an automated program proof system that runs in the background of a program editor. This system is called Spec# and attempts proving inlined assertions, while editing the program. If a proof fails, then either some annotation is needed or a code error has been found. More info in http://research.microsoft.com/en-us/projects/specsharp/

If you specify that a software language or its compiler should "self-verify" certain classes of programs and detect certain classes of errors or bugs, you need to be very careful about how you specify the class of programs and class of errors or bugs to be detected. If you choose classes of programs and errors too broadly you may accidentally be specifying a variation of the "Turing Halting Problem"--which was proven to be impossible in 1936 by Alan Turing himself, the father of computability theory. See

http://en.wikipedia.org/wiki/Halting_problem

for further details.

In one very general case, Turing's Halting Problem asks, "Can you write a program that can scan any other program as input, and determine whether or not that other program contains a bug such that it will NEVER terminate (halt) executing its instruction set?" And Alan Turing proved that such a "debugger program" could only exist if there was at one specifiable input program that it would fail to correctly debug. In other words, no such general debugging program can exist that works on all possible input programs. However for more limited cases of debugging, such as many of the cases described by writers above, a compiler/debugger can be designed to identify and warn the programmer about certain classes of undesirable program behavior.

You could also check out context-oriented programming languages, they are not big in verification, but some of them provide nice run-time and compile-time verification techniques.

You might take a look at NetRexx which has been released by IBM to RexxLA .

Haipeng: "For example, by running the compiled code with certain test inputs, the program will either output the correct results, or report the errors in the code ..."

There is a programming language and IDE that does this, it can be found at http://racket-lang.org/. Here's a simple Fah to Cel program with test cases:

(check-expect (f2c -40) -40)

(check-expect (f2c 32) 0)

(check-expect (f2c 212) 100)

(define (f2c f)

(* 5/9 (- f 32))

After compiling and running the program the Racket IDE outputs "All 3 tests passed!"

This sounds dangerously close to "I just want to tell the computer what I want, and let it figure out how". Verification by definition checks the operation of the program against the specific requirements of the program. There are syntactically strong requirements languages, like the "Z" requirements language, which can be used to generate "executable requirements". There are also many forms of "assert" or unit tests one can create (https://en.wikipedia.org/wiki/List_of_unit_testing_frameworks) - but that would hardly count as "self-verification".

In the end verification is always manual, either through preparation in the case of "Z" or adhoc, automated and programmer generated like unit tests.

Take a look on http://gpml.foi.hr/SCT_Autogenerator_Example/ . This is an example of Autogenerator, with introductory video. Autogenerator uses its specification, configuration and set of program artifacts to generate and execute immediately a necessary code to provide some particular operation (e.g. data review, edit, etc.) on user request. The concept uses the possibility of scripting languages (here Python) to evaluate the code from variables.

FORTH already does that for a very long time.

I'd like to see references concerning Forth and verification, self- or otherwise.

The difficulty in many of the methods described is to capture the *requirements*, in a rigorous and testable way in the first place. "Z" as a requirements tool got no traction in industry, not because it failed but because capturing requirements is *HARD*. It is far easier to leave in the vagueness of a natural language and leave the details to the implementers, the engineers. Agile design and management approaches have the advantage that the engineers capture the detailed requirements as unit tests and at least make the design requirements visible. This still begs the question of whether all the requirements designed to have been covered, or even whether the unit tests cover all of the code. Even when coverage of "user stories" and code is measured, improving the coverage is manual.

Aside of Forth, functional and logic programming languages tend to have much cleaner mathematical semantics than the imperative and OO languages that rely heavily on the state of the memory store and side effects, which makes it easier to weld the specification/verification with the code . For instance, Ciao Prolog uses the mechanism of assertions to specify and/or check the behavior of Prolog procedures, in terms of e.g., computational complexity, types, pre- and post-conditions, sharing (aliasing), termination (when possible), etc.

See:

http://www.sciencedirect.com/science/article/pii/S0167642305000468

How about incorporating machine learning principles into the self-test programming language compilers, by which programmers will not need do any thing different from what they do today but the compiler is clever enough to instrument things statistically so that the program will increase the self-governed bug reporting capabilities while it is run more and more times - it keeps learning about what are treated as bugs when users tell (or any other way to feedback) the program something was not correct.

You could take a look at Pyret (http://pyret.org), a vaguely Python-like teaching language in which the syntax rule for a function definition includes an associated block of test cases. I haven't used it yet, but it looks interesting.

And of course Racket (http://racket-lang.org), as mentioned above, has always paid a lot of attention to making it easy to write test cases, so maybe people will actually do it.