Anybody used such things? Can anybody compare/contrast with ATS? It
drives me crazy that things like MISRA exist at all, frankly. How
anybody can directly use C any more, I will never understand. 
Another one, I forget, a not so much sad: MISRA C comes with bridges to
proof assistants like Coq and Isabelle. I I my mind is right, the most
famous bridge is named Why (thatâs the name), but I canât find the web site
(you guess⊠with such a name, search result give irrelevant results)
I did not know that. That is quite possibly a very redeeming feature!
hi, Yeah, sorry I wasnât trying to ask if ATS could export MISRA-C
exactly. (Although I guess it would give ATS more leverage in the auto
industry if it did meet the MISRA requirements / passed their
linters.) I was just wondering if/how much ATS in general
addressed/resolved/avoided the high-level worries that motivate
MISRA-C.
For the already existing, I believe.
a fine point. a sad point. a realistic point.
Another one, I forget, a not so much sad: MISRA C comes with bridges to
proof assistants like Coq and Isabelle. I I my mind is right, the most
famous bridge is named Why (thatâs the name), but I canât find the web site
(you guess⊠with such a name, search result give irrelevant results)
As far as I can tell, the most reliable C programs are those automatically
generated from sources written in other languages or created by tools. I
donât know MISRA, but I suspect that generating MISRA C complicates the
underlying code generation and could thus potentially causing more bugs.On Wednesday, April 22, 2015 at 2:02:39 PM UTC-4, Raoul Duke wrote:
Anybody used such things? Can anybody compare/contrast with ATS? It
drives me crazy that things like MISRA exist at all, frankly. How
anybody can directly use C any more, I will never understand.
Anybody used such things? Can anybody compare/contrast with ATS? It
drives me crazy that things like MISRA exist at all, frankly. How
anybody can directly use C any more, I will never understand.
For the already existing, I believe.
I just read the paper called Defining the Undefinedness of C, Defining the Undefinedness of C | IDEALS.
I think the motivation behind MISRA-C and other similar benchmarks is to
avoid undefined behaviors in C programs because those undefinedness will
basically render a program meaningless. An undefined program can do
anything, observably right or wrong. Whether or not ATS has undefined
behavior is one thing, and whether its compiler generates C code that has
undefined behavior is another.On Thursday, April 23, 2015 at 2:30:31 PM UTC-4, Raoul Duke wrote:
hi, Yeah, sorry I wasnât trying to ask if ATS could export MISRA-C
exactly. (Although I guess it would give ATS more leverage in the auto
industry if it did meet the MISRA requirements / passed their
linters.) I was just wondering if/how much ATS in general
addressed/resolved/avoided the high-level worries that motivate
MISRA-C.
For the already existing, I believe.
a fine point. a sad point. a realistic point.
i wish we had a way to apply the DDD / refactoring approaches where
you try to carve the giant thing up into parts so you can find ways to
insert interfaces and gradually take it out into the parking lot and
shoot it dead, and replace it with something less horrible. being
killed by e.g. Toyotaâs (or, Iâm sure, most any other car companyâs)
crappy code that controls the fly-by-wire stuff these days is just
saaaaad.
The following keywords
project âWhyâ verify C
lead me to http://why3.lri.fr/
When I search for Java, itâs very easy to get links to the java library
documentation. For ATS, sometimes I have to use keyword Postiats to locate
the on-line documentation. Maybe we should form up certain guidance for
people to search ATS related resources on-line easily.On Wednesday, April 22, 2015 at 7:50:22 PM UTC-4, Yannick DuchĂȘne wrote:
Le jeudi 23 avril 2015 01:11:09 UTC+2, Raoul Duke a Ă©crit :
For the already existing, I believe.
a fine point. a sad point. a realistic point.
Another one, I forget, a not so much sad: MISRA C comes with bridges to
proof assistants like Coq and Isabelle. I I my mind is right, the most
famous bridge is named Why (thatâs the name), but I canât find the web site
(you guess⊠with such a name, search result give irrelevant results)