www.digitalmars.com         C & C++   DMDScript  

digitalmars.D - Re: Clay language

reply bearophile <bearophileHUGS lycos.com> writes:
Walter:

 Ada is a failed language.

I agree that as general purpose language Ada is probably a failed language. But currently Ada is often the best language still if you have to write the autopilot software for an aeroplane or something that requires software with minimal bug counts. Even if Ada is globally a failed language, it's a large language composed of many features, so some of its feature may be good still. D and Ada share some purposes and semantics, they are similar languages. They are both large system languages fit for very high performance systems, they are both improvements over older simpler languages (C-family and Pascal-family), both have generics, and so on (there are some differences too, where D tries to add very flexible and general features, Ada often adds many different specialized features that are safer. Ada doesn't value code compactness much). The most important shared design goal of Ada and D is that both regard program correctness as very important. In this regard surely Ada tries harder than D. I like Python for certain kinds of programs, but if I go on a ship that uses an autopilot I'd like it to be written in a language safer than C. D advertises itself as a language that cares a lot about code correctness, but I am sure more is doable in this regard. Even if today Ada is sometimes the best language to write an autopilot, tomorrow the situation may change. Microsoft keeps developing its Sing# language, and two Microsoft researchers have released "Verve", a little experimental operating system kernel that has a nucleus written in typed assembly statically verified, and Spec# or Sing# code... So maybe in future high integrity software systems will be written like this instead of Ada (typed assembly is nicer than the normal inline D asm even when it's not formally verified, just verified by the type system, more or less like C code). Bye, bearophile
Dec 29 2010
parent reply Walter Bright <newshound2 digitalmars.com> writes:
bearophile wrote:
 Walter:
 
 Ada is a failed language.

I agree that as general purpose language Ada is probably a failed language. But currently Ada is often the best language still if you have to write the autopilot software for an aeroplane or something that requires software with minimal bug counts.

I don't believe that has been objectively demonstrated. It's a claim.
 Even if today Ada is sometimes the best language to write an autopilot,
 tomorrow the situation may change. Microsoft keeps developing its Sing#
 language, and two Microsoft researchers have released "Verve", a little
 experimental operating system kernel that has a nucleus written in typed
 assembly statically verified, and Spec# or Sing# code... So maybe in future
 high integrity software systems will be written like this instead of Ada
 (typed assembly is nicer than the normal inline D asm even when it's not
 formally verified, just verified by the type system, more or less like C
 code).

Despite what the marketing literature on Spec# says, and what you repeated from that, I was able to show within minutes that its contract proving feature is so limited as to be effectively useless. Spec# doesn't do your hobby horse security features, either. In other words, I think you should be careful reading feature lists and lists of claims put out by marketing departments. Whether a language feature delivers on its promises is only born out by years of experience in the field writing real software with real programmers. The only way you're going to actually find out what is causing problems in the field is to talk a lot with experienced programmers and their managers, and doing things like reading the bug lists on major projects and trying to figure out why those problems happened. 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.
Dec 29 2010
parent reply bearophile <bearophileHUGS lycos.com> writes:
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
Dec 30 2010
parent Walter Bright <newshound2 digitalmars.com> writes:
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.
Dec 30 2010