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.
