Languages specifically designed to make static verification easier

A lot of languages (perhaps all of them) are design开发者_StackOverflowed to make writing programs easier. They all have different domains, and aim to simplify developing programs in these domains (C makes developing low-level programs easier, Java makes developing complex business logic easier, et al.). Perhaps other purposes are sacrificed in sake of writing and maintaining programs in an easier, more natural, less error-prone way.

Are there any languages specifically designed to make verification of source code--i.e. static analysis--easier? Of course, capability to write common programs for modern machines should also persist.

One of the design goals of Ada was to support a certian amount of formal verification. It was moderately successful, but verification didn't exactly take off like they were hoping. Luckily Ada is good for far more than that. Sadly, that hasn't helped it much either...

There's an Ada subset called Spark that keeps this alive today. Praxis sells a development suite built around it.

Are there any languages specifically designed to make verification of source code easier?

This was a vague goal of both the CLU and ML languages, but the only language design I know that takes static verification really seriously is Spark Ada.

Dijkstra's language of guarded commands (as described in Discipline of Programming) was designed to support static verification, but it was explicitly not supposed to be implemented.

Gerard Holzmann's Promela language was also designed for static analysis by the model checker SPIN, but again it's not executable.

Auditors in the E language provide a built-in means of writing code analyses within the language itself and requiring that some section of code pass some static check. You might also be interested in the related-work part of the paper.

I haven’t used it myself, so I can’t speak with any authority, but I understand that the Eiffel programming language was designed to use Code by Contracts, which would make static analysis much easier. I don’t know if that counts or not.

There is SAIL, the Static Analysis Intermediate Language or Flexibo

One has two problems in "making verification of source code easier". One is languages in which you don't do gross things such as arbitrary cases (such as C). Another is specifying what you want to verify, for that you need a good assertions languages.

While many languages have proposed such assertions languages, I think the EDA community has been pushing the envelope most effectively with temporal specifications. The "Property Specification Language" is a standard; you can learn more from P1850 Standard for PSL: Property Specification Language (IEEE-1850). One idea behind PSL is that you can add it to existing EDA languages; I think the EDA community has been incorporating into the EDA langauges as time goes by.

I've often wished for something like PSL to embed in conventional computer software.

Static verification is a bad start for this task. It's based on an assumption that it's possible to verify correctness of the program automatically. It's not feasible in real world, and expecting the program to check arbitrarily complex code without any hints is just plain dumb. Usually software for static verification ends up requiring hints all over source code, and in the end generates lots of false positives and false negatives. It has some niche, but that's it. (See introduction to "Types and programming languages" by Pierce)

While these kind of tools were developed by engineers for their own simple purposes, real solution have been baking in an academy. It was found that types in statically typed programming languages are equivalent to logic statements given everything goes smooth and language doesn't have some kind of bad behaviour. This is called "Curry-Howard correspondence", and the embedding of logic into types is "Brouwer-Heyting-Kolmogorov logic". The most powerful proofs are possible only in the languages with powerful types: dependent types. If we forget all this terminology for a while, this means that we can write programs that carry proofs of its own correctness, and these proofs are checked while the program gets compiled, with no executable file given in case of failure.

The positive side of this approach is that you never get any false negatives, i.e. compiled program is guaranteed to work properly according to the specification. Even without extra proofs about specification, programs in dependently-typed languages are less prone to mistakes, because divisions by zero, unhandled exceptions and overflows just never end up in an executable program.

Always writing such proofs by hand is tedious. For that there are "tactics", i.e. programs that generate proofs of correctness. These are almost equivalent to programs for static verification, but, unlike them, are required to generate formal proof.

There is a range of dependently-typed languages for different purposes: Coq, Agda, Idris, Epigram, Cayenne etc.

Tactics are implemented in Coq and probably several more languages. Also Coq is the most mature of them all, with infrastructure including libraries like Bedrock.

In case C code extraction from Coq is not enough for your requirements, you can use ATS, which is on par in performance with C.

Haskell employs weak form of Curry-Howard correspondence: it works fine, unless you start writing failing or forever-looping programs. In case your requirements are not that hard to write formal proofs, consider using Haskell.