Communications of the ACM,
Vol. 53 No. 12, Pages 56-66
10.1145/1859204.1859226
Only if the programmer can prove (through formal machine-checkable proofs) it is free of bugs with respect to a claim of dependability.
The full text of this article is premium content
1 Comments
Paul Valckenaers
Years ago, I followed a course on formal semantics... and, although I could follow all the theory and mathematics with little effort, I was uneasy with the material. More recently, I got to know the concept of an ontology, and realized that it covers concepts but not instances (i.e. a car but not your car parked in front of your office building). Suddenly, while studying Pi-calculus, I realized the cause of my uneasiness: those formal techniques, languages, ... could not even capture a real-world concept, and surely not its real-world instances. This is unfortunate since "dependability" is most relevant when the real world is involved in a physical manner. If certified software wants our respect, it should at least show evidence that it is trying to address the certification of "a person will not be stuck between computer-controlled doors" and if it happens "the subway train will not start moving with a person hanging halfway out of the wagon". Can anyone point me to publications looking into this matter? Which research is going beyond "the rewriting of computations"? I recognize the merit of "treating certification separately from ..." but I have to point out that there is little added value in reinforcing what already are the stronger links. It may be useful but does not merit priority over efforts looking at the weakest link (outside the comfort zones of research communities).
Displaying 1 comment
Log in to Read the Full Article
Purchase the Article
Log in
Create a Web Account
If you are an ACM member, Communications subscriber, Digital Library subscriber, or use your institution's subscription, please set up a web account to access premium content and site
features. If you are a SIG member or member of the general public, you may set up a web account to comment on free articles and sign up for email alerts.
![[article image]](https://cacm.acm.org/system/assets/0000/4272/112010_CACMpg57_Certified-Software_A.large.jpg?1476779419&1290117098 "Certified Software illustration")
Paul Valckenaers
Years ago, I followed a course on formal semantics... and, although I could follow all the theory and mathematics with little effort, I was uneasy with the material. More recently, I got to know the concept of an ontology, and realized that it covers concepts but not instances (i.e. a car but not your car parked in front of your office building). Suddenly, while studying Pi-calculus, I realized the cause of my uneasiness: those formal techniques, languages, ... could not even capture a real-world concept, and surely not its real-world instances. This is unfortunate since "dependability" is most relevant when the real world is involved in a physical manner. If certified software wants our respect, it should at least show evidence that it is trying to address the certification of "a person will not be stuck between computer-controlled doors" and if it happens "the subway train will not start moving with a person hanging halfway out of the wagon". Can anyone point me to publications looking into this matter? Which research is going beyond "the rewriting of computations"? I recognize the merit of "treating certification separately from ..." but I have to point out that there is little added value in reinforcing what already are the stronger links. It may be useful but does not merit priority over efforts looking at the weakest link (outside the comfort zones of research communities).