Clay language

[bearophile]

Walter:

> I don't believe that has been objectively demonstrated. It's a claim.

Here at page 6 (Table 1) you see some bug frequencies for various languages, C, Ada, SPARK, etc:
http://www.cs.virginia.edu/~jck/cs686/papers/andy.german.pdf
(This is not a demonstration).


> Despite what the marketing literature on Spec# says, and what you repeated from that,

You and Andrei write D marketing all the time :-)


> I was able to show within minutes that its contract proving feature is so
> limited as to be effectively useless.

You have found that if you use a specific solver (I think S3, but other solvers are pluggable in Spec#) the solver was unable to demonstrate your specific code. Elsewhere I have read that bitwise operations are harder for such solvers.

A design requirement of the Verve Kernel is to have some of its most important parts demonstrated as correct. So where the automatic solver is not able to do its work, you have to demonstrate the code manually (or with a semi-automatic solver). So the better the automatic solver is, the less work you have to do. But even if it's able to demonstrate only half of the code, you have saved lot of manual work. So it's not useless. You can't find an automated theorem prover able to demonstrate code in all cases.


> I do have some experience with this, having worked at Boeing on flight critical
> designs for airliners. There are a lot of lessons there applicable to software
> development, and one lesson is that armchair gedanken experiments are no
> substitute for field experience in how mechanics actually put things together,
> what kinds of mistakes they are prone to making, etc.

But informatics is not just engineering, it's a branch of mathematics too. It's important to study new nice armchair gedanken experiments, think about them, develop them. I have some experience with science and computer science, and I can tell those Microsoft researchers are doing some quite interesting computer science. Please don't make the digitalmars newsgroups too much academic-unfriendly :-) D2 is too much young to compensate for the loss of such people from its community.

Bye,
bearophile