Clay language

[Walter Bright]

bearophile wrote:
> 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).

Thank you. I think that looks like solid information, what I was asking for. I'd 
be curious how D stacks up under such analysis.


>> Despite what the marketing literature on Spec# says, and what you repeated
>> from that,
> 
> You and Andrei write D marketing all the time :-)

Yes, we do.


>> 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.

This demonstrated to me that Spec# is a research project. It is not something 
that is remotely ready for production use. It simply does not deliver on its 
promises.


> 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.

It's another research project.


>> 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.

D isn't a research project. It is much like an airliner - you don't use an 
airliner as a research project. It's a workhorse. You use it to move passengers 
with safety and efficiency, using the best available proven technology.

A lot of what D does has been proven effective in other languages, but I admit 
that the mix of features as expressed in D can have unexpected consequences, and 
only time & experience will tell if we got the recipe right or not.