On 15/09/18 18:32, Stefan Reuther wrote:> Am 14.09.2018 um 20:56 schrieb David Brown: >> On 14/09/18 19:57, Stefan Reuther wrote: >>> Am 14.09.2018 um 12:26 schrieb David Brown: >>>> No, it is not - not for decades. In C, "string" is defined in 7.1.1 of >>>> the current standard as "A string is a contiguous sequence of characters >>>> terminated by and including the first null character." >>> >>> That is the library definition of "string". The language definition of a >>> string literal is in §6.4.5 which says: >>> >>> # In translation phase 7, a byte or code of value zero is appended to >>> # each multibyte character sequence that results from a string literal >>> # or literals. The multibyte character sequence is then used to >>> # initialize an array of static storage duration and length just >>> # sufficient to contain the sequence. [...] >>> >>> (paragraph 5 in ISO 9899:1999, paragraph 6 in n1548) >> >> Yes, I know the difference between a string and a string literal - I >> said that in a bit you snipped. >> >> And the library definition of a "string" /is/ the C definition of >> "string". The term is italicised in 7.1.1, denoting that it is defined >> in that paragraph. > > The library makes no mention of storage classes, meaning: it does not > care about storage classes. > > The language defines what happens with a string literal in §6.4.5p5/6, > namely: construction of an array of static storage duration, with > content that - lo and behold - fulfils the library's requirements of a > string, by being a zero-terminated array of characters.Ah - 6.4.5p6, second sentence: "The multibyte character sequence is then used to initialize an array of static storage duration and length just sufficient to contain the sequence." Key here is that that the standards specifically say that this array has "static storage duration". So yes, the OP's code is fine according to the C standard. Thank you for leading me to this point.> >> I know that's what the OP's code needs in order to be correct - the >> question is if the C standards guarantee that his code does what he wants. > > The question was: is a string literal's address and content valid after > the function containing it exits? The answer is: yes. >Agreed (now that I have seen the light).>>> TL;DR: OP's code is safe, language-wise. >> >> Can you back that up with references to the standard? > > See above. >Thank you.> > Stefan >
arm-gcc: pointer to constant string
Started by ●September 14, 2018
Reply by ●September 16, 20182018-09-16
Reply by ●September 16, 20182018-09-16
On 16/09/18 14:00, David Brown wrote:> On 15/09/18 18:28, Tom Gardner wrote: >> On 15/09/18 15:24, David Brown wrote: >>> On 14/09/18 21:51, Tom Gardner wrote: >>>> On 14/09/18 19:37, David Brown wrote: >>>>> On 14/09/18 19:45, Tom Gardner wrote: >>>>>> On 14/09/18 16:02, David Brown wrote: >>> >>> <snip> >>> >>>>>>> With C, there are three standards to choose from - C90, C99 and C11. >>>>>>> (There is an upcoming C17, but it is basically a bug-fix and occasional >>>>>>> improved wording, so there is not much to be found there except nicer >>>>>>> typesetting.) >>>>>>> >>>>>>> And there are also implementation-specific extensions - both compiler >>>>>>> specific and target-specific. >>>>>> >>>>>> Don't forget the commercially important /subsets/! The need >>>>>> for subsets is a warning flag in itself. >>>>>> >>>>> >>>>> What need of "commercially important subsets" are you talking about? >>>> >>>> MISRA-C, for example. >>> >>> That is a set of rules for C, rather than a subset as such. >> >> That's hairsplitting, which obscures rather than illuminates. > > It is no different than programming in Forth, Ada, Python, Fortran, or any other > language. What makes you think C is special? > >> >> >>> (And 90% of it could be replaced by three rules - 1. Learn the language >>> properly and don't write invalid code. 2. Write in a readable fashion. 3. >>> Get proper tools and learn how to use them.) >> >> Nonsense. > > You haven't read the Misra rules, have you? I didn't mention that the remaining > 10% of the rules go against the C standards and compiler norms by inventing > their own non-standard type system. I suppose that /does/ mean it counts as > another type of C, but it is certainly not a standard one.If the type system is a valid use of C, then it is no more non-standard than libraries that aren't defined in the standard.>>> Of course if a specific task, project, employer or customer has rules for how >>> you work, you need to know them and follow them. But that is not "a subset >>> of the language", or the fault of the language. >> >> I know of three languages where subsetting is a practical >> necessity: C, C++, and the SPARK subset of Ada. That's >> significant. > > I think you'll find it applies to /all/ programming languages. For some > languages, there is enough consensus in these "subsets" and enough popularity of > them that they are known popularly - like SPARK and MISRA. For others, they > will be smaller. If company guidelines say that when programming Python you > must use capital letters for class names and never write "from module import *", > then you have a subset of the language just as surely as if they say "use MISRA > for C".I think most people would look askance at that being an informative definition of "subset" - and would instantly think to look at what's being concealed.>> However SPARK's objective and *ability* is something that >> C/C++ cannot even dream of: provably correct implementation >> for use in high integrity systems. To get that you would have >> to subset /any/ language (except possible NewSpeak!). >> > > I know that is SPARK's objective. Most sets of guidelines or coding standards > aim towards more reliable and less error-prone coding (though few aspire to > claiming they can be provably correct).Agreed. Overall I'm not a fan of formal proofs except in a few very niche applications. The proofs always have hard (in multiple senses) boundaries which exclude important real-world problems.>>>>> There /are/ compilers that implement subsets of C standards. But I don't >>>>> see a /need/ for them. >>>>> >>>>>> >>>>>> >>>>>>> Generally, it is not hard to know which C version you are dealing with, >>>>>>> and there is very little code that is valid in one version that is not >>>>>>> equally valid in later versions. >>>>>> >>>>>> That statement, while correct, skims over a significant problem: >>>>>> unfortunately too few people understand and can /predict/ what is >>>>>> valid and invalid. >>>>> >>>>> Of course they can. Very few people ever write code that is valid C90 code >>>>> and not valid C99 or C11 code. There are /very/ few incompatibilities. >>>>> About the only one of significance I can think of is that functions no >>>>> longer have implicit declarations. What examples can you give of >>>>> reasonable, valid C90 code that is not C99 compatible, or C99 code that is >>>>> not C11 compatible? Or C99 code that is not gnu99 compatible? >>>> >>>> You miss my point. >>> >>> Not unlikely! >>> >>>> >>>> I am not arguing about the /differences/ between, say C99 and C11, >>>> but C of /any/ standard. >>> >>> I still don't get it. Do you mean, say, the difference between C99 on gcc >>> and C99 on IAR ? Or the difference between C on an ARM and C on an AVR? >> >> No. Very, /very/ few - if any - developers understand >> all the undefined and implementation defined behaviour >> of any standard of C or C++, and how to reconcile different >> parts of the same standard (or differing implementations >> of the same standard)! > > I think I see what you are getting at now - you are saying there are things in C > that are undefined (or implementation-defined) that many C programmers don't > realise are a problem. Yes, I can agree with that - though I think the problem > is often overrated. The great majority of undefined behaviour in C is obviously > undefined because there is no sensible definition for it - and there is no way > anyone could reasonably expect code to "work". That applies to things like > buffer overruns, out of bounds pointers, etc. The most obvious category of > undefined behaviours where people get things wrong are, I would say, accessing > data through incompatible pointers and signed integer overflow. In the case of > signed integer overflow, the code is almost certainly wrong regardless of any > definition of the behaviour. > > The rest is just a matter of not knowing the language as well as they should, > and thus getting things wrong. That happens in all languages. > > I am not in any way saying that C or C++ are perfect languages, or that their > standards are ideal, or anything like that. I am merely saying they are not as > bad as many people make out, and not different in principle from other languages.There are no perfect languages, and probably cannot be. However, some languages are significantly more/less imperfect in practical use than others. Overall C has expanded until its rough edges have become part of the problem rather than part of the solution. Once it really was the best language for many purposes - but we have learned Better Techniques in the past 40 years. Cs position is firm for the same reason than COBOL's position is firm: history, familiarity and weight of existing code.
Reply by ●September 16, 20182018-09-16
On 16/09/18 15:33, Tom Gardner wrote:> On 16/09/18 14:00, David Brown wrote: >> On 15/09/18 18:28, Tom Gardner wrote: >>> On 15/09/18 15:24, David Brown wrote: >>>> On 14/09/18 21:51, Tom Gardner wrote: >>>>> On 14/09/18 19:37, David Brown wrote: >>>>>> On 14/09/18 19:45, Tom Gardner wrote: >>>>>>> On 14/09/18 16:02, David Brown wrote: >>>> >>>> <snip> >>>> >>>>>>>> With C, there are three standards to choose from - C90, C99 and >>>>>>>> C11. >>>>>>>> (There is an upcoming C17, but it is basically a bug-fix and >>>>>>>> occasional >>>>>>>> improved wording, so there is not much to be found there except >>>>>>>> nicer >>>>>>>> typesetting.) >>>>>>>> >>>>>>>> And there are also implementation-specific extensions - both >>>>>>>> compiler >>>>>>>> specific and target-specific. >>>>>>> >>>>>>> Don't forget the commercially important /subsets/! The need >>>>>>> for subsets is a warning flag in itself. >>>>>>> >>>>>> >>>>>> What need of "commercially important subsets" are you talking about? >>>>> >>>>> MISRA-C, for example. >>>> >>>> That is a set of rules for C, rather than a subset as such. >>> >>> That's hairsplitting, which obscures rather than illuminates. >> >> It is no different than programming in Forth, Ada, Python, Fortran, or >> any other language. What makes you think C is special? >> >>> >>> >>>> (And 90% of it could be replaced by three rules - 1. Learn the >>>> language properly and don't write invalid code. 2. Write in a >>>> readable fashion. 3. Get proper tools and learn how to use them.) >>> >>> Nonsense. >> >> You haven't read the Misra rules, have you? I didn't mention that the >> remaining 10% of the rules go against the C standards and compiler >> norms by inventing their own non-standard type system. I suppose that >> /does/ mean it counts as another type of C, but it is certainly not a >> standard one. > > If the type system is a valid use of C, then it is no more > non-standard than libraries that aren't defined in the standard. >Unfortunately, MISRA's idea of "essential types" is not /quite/ compatible with actual C. I have forgotten the details (and they may vary between MISRA versions), but there are points in which the MISRA rules say code should do something that is different from what the C rules say. I have seen at least one case where a (massively expensive) compiler generated code regarding integer promotions that was "MISRA correct" but not "C standards correct".> > >>>> Of course if a specific task, project, employer or customer has >>>> rules for how you work, you need to know them and follow them. But >>>> that is not "a subset of the language", or the fault of the language. >>> >>> I know of three languages where subsetting is a practical >>> necessity: C, C++, and the SPARK subset of Ada. That's >>> significant. >> >> I think you'll find it applies to /all/ programming languages. For >> some languages, there is enough consensus in these "subsets" and >> enough popularity of them that they are known popularly - like SPARK >> and MISRA. For others, they will be smaller. If company guidelines >> say that when programming Python you must use capital letters for >> class names and never write "from module import *", then you have a >> subset of the language just as surely as if they say "use MISRA for C". > > I think most people would look askance at that being an informative > definition of "subset" - and would instantly think to look at what's > being concealed. > > >>> However SPARK's objective and *ability* is something that >>> C/C++ cannot even dream of: provably correct implementation >>> for use in high integrity systems. To get that you would have >>> to subset /any/ language (except possible NewSpeak!). >>> >> >> I know that is SPARK's objective. Most sets of guidelines or coding >> standards aim towards more reliable and less error-prone coding >> (though few aspire to claiming they can be provably correct). > > Agreed. > > Overall I'm not a fan of formal proofs except in a few very > niche applications. The proofs always have hard (in multiple > senses) boundaries which exclude important real-world problems.There are few cases where formal proofs are worth the time and costs involved. But I like - when possible - to write my code with a view that a formal proof /could/ be made if someone were to go to the effort. It is rare that you could prove a whole program - but not uncommon that you could (if you wanted to) prove many of the functions involved. Thinking in terms of pre-conditions, invariants, post-conditions, variants, specifications - that is all good stuff for writing solid code, even if you don't do so formally.> > >>>>>> There /are/ compilers that implement subsets of C standards. But >>>>>> I don't see a /need/ for them. >>>>>> >>>>>>> >>>>>>> >>>>>>>> Generally, it is not hard to know which C version you are >>>>>>>> dealing with, >>>>>>>> and there is very little code that is valid in one version that >>>>>>>> is not >>>>>>>> equally valid in later versions. >>>>>>> >>>>>>> That statement, while correct, skims over a significant problem: >>>>>>> unfortunately too few people understand and can /predict/ what is >>>>>>> valid and invalid. >>>>>> >>>>>> Of course they can. Very few people ever write code that is valid >>>>>> C90 code and not valid C99 or C11 code. There are /very/ few >>>>>> incompatibilities. About the only one of significance I can think >>>>>> of is that functions no longer have implicit declarations. What >>>>>> examples can you give of reasonable, valid C90 code that is not >>>>>> C99 compatible, or C99 code that is not C11 compatible? Or C99 >>>>>> code that is not gnu99 compatible? >>>>> >>>>> You miss my point. >>>> >>>> Not unlikely! >>>> >>>>> >>>>> I am not arguing about the /differences/ between, say C99 and C11, >>>>> but C of /any/ standard. >>>> >>>> I still don't get it. Do you mean, say, the difference between C99 >>>> on gcc and C99 on IAR ? Or the difference between C on an ARM and C >>>> on an AVR? >>> >>> No. Very, /very/ few - if any - developers understand >>> all the undefined and implementation defined behaviour >>> of any standard of C or C++, and how to reconcile different >>> parts of the same standard (or differing implementations >>> of the same standard)! >> >> I think I see what you are getting at now - you are saying there are >> things in C that are undefined (or implementation-defined) that many C >> programmers don't realise are a problem. Yes, I can agree with that - >> though I think the problem is often overrated. The great majority of >> undefined behaviour in C is obviously undefined because there is no >> sensible definition for it - and there is no way anyone could >> reasonably expect code to "work". That applies to things like buffer >> overruns, out of bounds pointers, etc. The most obvious category of >> undefined behaviours where people get things wrong are, I would say, >> accessing data through incompatible pointers and signed integer >> overflow. In the case of signed integer overflow, the code is almost >> certainly wrong regardless of any definition of the behaviour. >> >> The rest is just a matter of not knowing the language as well as they >> should, and thus getting things wrong. That happens in all languages. >> >> I am not in any way saying that C or C++ are perfect languages, or >> that their standards are ideal, or anything like that. I am merely >> saying they are not as bad as many people make out, and not different >> in principle from other languages. > > There are no perfect languages, and probably cannot be. > > However, some languages are significantly more/less > imperfect in practical use than others. > > Overall C has expanded until its rough edges have become > part of the problem rather than part of the solution. Once > it really was the best language for many purposes - but we > have learned Better Techniques in the past 40 years.Certainly I do not think C is the best choice of language for many of the types of use it is put to. I think most people who program in C would be more productive and write more correct code in other languages - and most programs that are written in C would be better written in other languages.> > Cs position is firm for the same reason than COBOL's position > is firm: history, familiarity and weight of existing code.Those are undoubtedly reasons for choosing C in many cases. But C is still the best choice for many purposes - and sometimes the only "choice".
Reply by ●September 16, 20182018-09-16
On 16/09/18 21:06, David Brown wrote:> On 16/09/18 15:33, Tom Gardner wrote: >> On 16/09/18 14:00, David Brown wrote: >>> On 15/09/18 18:28, Tom Gardner wrote: >>>> On 15/09/18 15:24, David Brown wrote: >>>>> On 14/09/18 21:51, Tom Gardner wrote: >>>>>> On 14/09/18 19:37, David Brown wrote: >>>>>>> On 14/09/18 19:45, Tom Gardner wrote: >>>>>>>> On 14/09/18 16:02, David Brown wrote: >>>>> >>>>> <snip> >>>>> >>>>>>>>> With C, there are three standards to choose from - C90, C99 and C11. >>>>>>>>> (There is an upcoming C17, but it is basically a bug-fix and occasional >>>>>>>>> improved wording, so there is not much to be found there except nicer >>>>>>>>> typesetting.) >>>>>>>>> >>>>>>>>> And there are also implementation-specific extensions - both compiler >>>>>>>>> specific and target-specific. >>>>>>>> >>>>>>>> Don't forget the commercially important /subsets/! The need >>>>>>>> for subsets is a warning flag in itself. >>>>>>>> >>>>>>> >>>>>>> What need of "commercially important subsets" are you talking about? >>>>>> >>>>>> MISRA-C, for example. >>>>> >>>>> That is a set of rules for C, rather than a subset as such. >>>> >>>> That's hairsplitting, which obscures rather than illuminates. >>> >>> It is no different than programming in Forth, Ada, Python, Fortran, or any >>> other language. What makes you think C is special? >>> >>>> >>>> >>>>> (And 90% of it could be replaced by three rules - 1. Learn the language >>>>> properly and don't write invalid code. 2. Write in a readable fashion. 3. >>>>> Get proper tools and learn how to use them.) >>>> >>>> Nonsense. >>> >>> You haven't read the Misra rules, have you? I didn't mention that the >>> remaining 10% of the rules go against the C standards and compiler norms by >>> inventing their own non-standard type system. I suppose that /does/ mean it >>> counts as another type of C, but it is certainly not a standard one. >> >> If the type system is a valid use of C, then it is no more >> non-standard than libraries that aren't defined in the standard. >> > > Unfortunately, MISRA's idea of "essential types" is not /quite/ compatible with > actual C. I have forgotten the details (and they may vary between MISRA > versions), but there are points in which the MISRA rules say code should do > something that is different from what the C rules say. I have seen at least one > case where a (massively expensive) compiler generated code regarding integer > promotions that was "MISRA correct" but not "C standards correct". > >> >> >>>>> Of course if a specific task, project, employer or customer has rules for >>>>> how you work, you need to know them and follow them. But that is not "a >>>>> subset of the language", or the fault of the language. >>>> >>>> I know of three languages where subsetting is a practical >>>> necessity: C, C++, and the SPARK subset of Ada. That's >>>> significant. >>> >>> I think you'll find it applies to /all/ programming languages. For some >>> languages, there is enough consensus in these "subsets" and enough popularity >>> of them that they are known popularly - like SPARK and MISRA. For others, >>> they will be smaller. If company guidelines say that when programming Python >>> you must use capital letters for class names and never write "from module >>> import *", then you have a subset of the language just as surely as if they >>> say "use MISRA for C". >> >> I think most people would look askance at that being an informative definition >> of "subset" - and would instantly think to look at what's being concealed. >> >> >>>> However SPARK's objective and *ability* is something that >>>> C/C++ cannot even dream of: provably correct implementation >>>> for use in high integrity systems. To get that you would have >>>> to subset /any/ language (except possible NewSpeak!). >>>> >>> >>> I know that is SPARK's objective. Most sets of guidelines or coding >>> standards aim towards more reliable and less error-prone coding (though few >>> aspire to claiming they can be provably correct). >> >> Agreed. >> >> Overall I'm not a fan of formal proofs except in a few very >> niche applications. The proofs always have hard (in multiple >> senses) boundaries which exclude important real-world problems. > > There are few cases where formal proofs are worth the time and costs involved. > But I like - when possible - to write my code with a view that a formal proof > /could/ be made if someone were to go to the effort. It is rare that you could > prove a whole program - but not uncommon that you could (if you wanted to) prove > many of the functions involved. Thinking in terms of pre-conditions, invariants, > post-conditions, variants, specifications - that is all good stuff for writing > solid code, even if you don't do so formally. > >> >> >>>>>>> There /are/ compilers that implement subsets of C standards. But I don't >>>>>>> see a /need/ for them. >>>>>>> >>>>>>>> >>>>>>>> >>>>>>>>> Generally, it is not hard to know which C version you are dealing with, >>>>>>>>> and there is very little code that is valid in one version that is not >>>>>>>>> equally valid in later versions. >>>>>>>> >>>>>>>> That statement, while correct, skims over a significant problem: >>>>>>>> unfortunately too few people understand and can /predict/ what is >>>>>>>> valid and invalid. >>>>>>> >>>>>>> Of course they can. Very few people ever write code that is valid C90 >>>>>>> code and not valid C99 or C11 code. There are /very/ few >>>>>>> incompatibilities. About the only one of significance I can think of is >>>>>>> that functions no longer have implicit declarations. What examples can >>>>>>> you give of reasonable, valid C90 code that is not C99 compatible, or C99 >>>>>>> code that is not C11 compatible? Or C99 code that is not gnu99 compatible? >>>>>> >>>>>> You miss my point. >>>>> >>>>> Not unlikely! >>>>> >>>>>> >>>>>> I am not arguing about the /differences/ between, say C99 and C11, >>>>>> but C of /any/ standard. >>>>> >>>>> I still don't get it. Do you mean, say, the difference between C99 on gcc >>>>> and C99 on IAR ? Or the difference between C on an ARM and C on an AVR? >>>> >>>> No. Very, /very/ few - if any - developers understand >>>> all the undefined and implementation defined behaviour >>>> of any standard of C or C++, and how to reconcile different >>>> parts of the same standard (or differing implementations >>>> of the same standard)! >>> >>> I think I see what you are getting at now - you are saying there are things >>> in C that are undefined (or implementation-defined) that many C programmers >>> don't realise are a problem. Yes, I can agree with that - though I think the >>> problem is often overrated. The great majority of undefined behaviour in C >>> is obviously undefined because there is no sensible definition for it - and >>> there is no way anyone could reasonably expect code to "work". That applies >>> to things like buffer overruns, out of bounds pointers, etc. The most >>> obvious category of undefined behaviours where people get things wrong are, I >>> would say, accessing data through incompatible pointers and signed integer >>> overflow. In the case of signed integer overflow, the code is almost >>> certainly wrong regardless of any definition of the behaviour. >>> >>> The rest is just a matter of not knowing the language as well as they should, >>> and thus getting things wrong. That happens in all languages. >>> >>> I am not in any way saying that C or C++ are perfect languages, or that their >>> standards are ideal, or anything like that. I am merely saying they are not >>> as bad as many people make out, and not different in principle from other >>> languages. >> >> There are no perfect languages, and probably cannot be. >> >> However, some languages are significantly more/less >> imperfect in practical use than others. >> >> Overall C has expanded until its rough edges have become >> part of the problem rather than part of the solution. Once >> it really was the best language for many purposes - but we >> have learned Better Techniques in the past 40 years. > > Certainly I do not think C is the best choice of language for many of the types > of use it is put to. I think most people who program in C would be more > productive and write more correct code in other languages - and most programs > that are written in C would be better written in other languages. > >> >> Cs position is firm for the same reason than COBOL's position >> is firm: history, familiarity and weight of existing code. > > Those are undoubtedly reasons for choosing C in many cases. But C is still the > best choice for many purposes - and sometimes the only "choice".Oh dear. I can't find /anything/ to disagree with in those statements :)
Reply by ●September 17, 20182018-09-17
David Brown wrote:> On 16/09/18 15:33, Tom Gardner wrote: >> On 16/09/18 14:00, David Brown wrote:<snip>> > There are few cases where formal proofs are worth the time and costs > involved. But I like - when possible - to write my code with a view > that a formal proof /could/ be made if someone were to go to the effort. > It is rare that you could prove a whole program - but not uncommon > that you could (if you wanted to) prove many of the functions involved. > Thinking in terms of pre-conditions, invariants, post-conditions, > variants, specifications - that is all good stuff for writing solid > code, even if you don't do so formally. >If you stick to something akin to the Haskell Actor model and everything is an event, it's not too onerous to use combinators to generate a significant subset of all messages. With the proper level of introspection, you can "prove" the program works to a limit enumerated by the test vectors and that it continues to do so as changes are made to the code base. The test vectors and captured output can be controlled and compared to. And if you want to go as far as model checking or partial model checking, you have the stuff in place to enforce that now. Obviously, there are domains where you just can't get close enough to this ideal. So you gamble. <snip>> > Certainly I do not think C is the best choice of language for many of > the types of use it is put to. I think most people who program in C > would be more productive and write more correct code in other languages > - and most programs that are written in C would be better written in > other languages. >Possibly. But what C offers is the ability to build nonstandard, hybrid "furniture" to support the development effort that can not be forseen by language and library designers. This is especially pronounced in serialization and the ability to dynamically configure a program ( which are two sides of the same coin ). C also supports event-driven-ness in a way that few other languages do. <snip> -- Les Cargill
Reply by ●September 18, 20182018-09-18
On 18/09/18 04:24, Les Cargill wrote:> David Brown wrote: >> On 16/09/18 15:33, Tom Gardner wrote: >>> On 16/09/18 14:00, David Brown wrote: > <snip> >> >> There are few cases where formal proofs are worth the time and costs >> involved. But I like - when possible - to write my code with a view >> that a formal proof /could/ be made if someone were to go to the >> effort. It is rare that you could prove a whole program - but not >> uncommon that you could (if you wanted to) prove many of the functions >> involved. Thinking in terms of pre-conditions, invariants, >> post-conditions, variants, specifications - that is all good stuff for >> writing solid code, even if you don't do so formally. >> > > If you stick to something akin to the Haskell Actor model and everything > is an event, it's not too onerous to use combinators to generate a > significant subset of all messages. With the proper level of > introspection, you can "prove" the program works to a limit > enumerated by the test vectors and that it continues to do so as > changes are made to the code base. >Testing can /never/ prove a program is correct - unless you can enumerate /all/ inputs and states of your code and go through them all. Testing can prove a program is wrong (and it is vital for that), but it cannot prove a program is correct. A functional programming language like Haskell gives you a much better chance of actually proving the correctness of your code than an imperative language like C - that is one of the reasons for the existence of functional programming languages (it is the lack of state and side-effects that help). But if you want to prove the correctness of your Haskell program, you do it by an analysis of the code, or by deriving correct code in the first place - you don't do it by testing.> The test vectors and captured output can be controlled and > compared to. And if you want to go as far as model > checking or partial model checking, you have the stuff in place to > enforce that now. > > > Obviously, there are domains where you just can't get close enough to > this ideal. So you gamble. >Indeed - and almost all practical situations fall into this category.> <snip> > >> >> Certainly I do not think C is the best choice of language for many of >> the types of use it is put to. I think most people who program in C >> would be more productive and write more correct code in other >> languages - and most programs that are written in C would be better >> written in other languages. >> > > Possibly. But what C offers is the ability to build nonstandard, hybrid > "furniture" to support the development effort that can not be > forseen by language and library designers. This is especially pronounced > in serialization and the ability to dynamically configure a program ( > which are two sides of the same coin ). >I don't follow that at all.> C also supports event-driven-ness in a way that few other languages do. >And I follow that even less. (I am not saying I disagree with you, I just can't see what you are trying to say. Maybe I'll understand it better after some coffee.) C certainly has its important features and strengths, and is a very useful language to have.
Reply by ●September 18, 20182018-09-18
On 18/09/18 03:24, Les Cargill wrote:> David Brown wrote: >> On 16/09/18 15:33, Tom Gardner wrote: >>> On 16/09/18 14:00, David Brown wrote: > <snip> >> >> There are few cases where formal proofs are worth the time and costs >> involved. But I like - when possible - to write my code with a view that a >> formal proof /could/ be made if someone were to go to the effort. It is rare >> that you could prove a whole program - but not uncommon that you could (if you >> wanted to) prove many of the functions involved. Thinking in terms of >> pre-conditions, invariants, post-conditions, variants, specifications - that >> is all good stuff for writing solid code, even if you don't do so formally. >> > > If you stick to something akin to the Haskell Actor model and everything is an > event, it's not too onerous to use combinators to generate a significant subset > of all messages. With the proper level of introspection, you can "prove" the > program works to a limit > enumerated by the test vectors and that it continues to do so as > changes are made to the code base. > > The test vectors and captured output can be controlled and > compared to. And if you want to go as far as model > checking or partial model checking, you have the stuff in place to enforce that > now.That's nothing to do with formal proofs, of course. It is equivalent to "inspecting quality into a product". Yes, it is better than nothing/eyeballs - both of which I've witnessed :(> Obviously, there are domains where you just can't get close enough to this > ideal. So you gamble. > > <snip> > >> >> Certainly I do not think C is the best choice of language for many of the >> types of use it is put to. I think most people who program in C would be more >> productive and write more correct code in other languages - and most programs >> that are written in C would be better written in other languages. >> > > Possibly. But what C offers is the ability to build nonstandard, hybrid > "furniture" to support the development effort that can not be > forseen by language and library designers. This is especially pronounced in > serialization and the ability to dynamically configure a program ( which are > two sides of the same coin ). > > C also supports event-driven-ness in a way that few other languages do.Er, no. Event-driven programming is used at all levels of the application protocol stack. Frequently events/messages are layered on top of events/messages at other levels without the implementers even realising it. For examples, start by looking at telecoms and fintech applications - which are often written in Java :) (Including high frequency trading where they spend billions (literally) to shave ms off comms latency, and encode business rules in FPGA hardware!)
Reply by ●September 18, 20182018-09-18
On 18/09/18 09:32, Tom Gardner wrote:> On 18/09/18 03:24, Les Cargill wrote: >> David Brown wrote: >>> On 16/09/18 15:33, Tom Gardner wrote: >>>> On 16/09/18 14:00, David Brown wrote: >> <snip> >>> >>> There are few cases where formal proofs are worth the time and costs >>> involved. But I like - when possible - to write my code with a view >>> that a formal proof /could/ be made if someone were to go to the >>> effort. It is rare that you could prove a whole program - but not >>> uncommon that you could (if you wanted to) prove many of the >>> functions involved. Thinking in terms of pre-conditions, invariants, >>> post-conditions, variants, specifications - that is all good stuff >>> for writing solid code, even if you don't do so formally. >>> >> >> If you stick to something akin to the Haskell Actor model and >> everything is an event, it's not too onerous to use combinators to >> generate a significant subset of all messages. With the proper level >> of introspection, you can "prove" the program works to a limit >> enumerated by the test vectors and that it continues to do so as >> changes are made to the code base. >> >> The test vectors and captured output can be controlled and >> compared to. And if you want to go as far as model >> checking or partial model checking, you have the stuff in place to >> enforce that now. > > That's nothing to do with formal proofs, of course. > > It is equivalent to "inspecting quality into a product". > > Yes, it is better than nothing/eyeballs - both of which > I've witnessed :( > > >> Obviously, there are domains where you just can't get close enough to >> this ideal. So you gamble. >> >> <snip> >> >>> >>> Certainly I do not think C is the best choice of language for many of >>> the types of use it is put to. I think most people who program in C >>> would be more productive and write more correct code in other >>> languages - and most programs that are written in C would be better >>> written in other languages. >>> >> >> Possibly. But what C offers is the ability to build nonstandard, >> hybrid "furniture" to support the development effort that can not be >> forseen by language and library designers. This is especially >> pronounced in serialization and the ability to dynamically configure a >> program ( which are two sides of the same coin ). >> >> C also supports event-driven-ness in a way that few other languages do. > > Er, no. > > Event-driven programming is used at all levels of the application > protocol stack. Frequently events/messages are layered on top of > events/messages at other levels without the implementers even > realising it. >Windows gui apps are often written as event-driven code, and no one sane writes them in C - they use C++, Python, Delphi, Java, C#, VB, or many other languages. None of these are particularly specialised for events or messages, but they all work at least as well or better than C for it. Go is perhaps a good choice for event-driven code (I base that on absolutely zero experience with Go...).> For examples, start by looking at telecoms and fintech > applications - which are often written in Java :) (Including > high frequency trading where they spend billions (literally) > to shave ms off comms latency, and encode business rules > in FPGA hardware!)And if they want code that works reliably (and can prove it), they use Erlang rather than Java.
Reply by ●September 22, 20182018-09-22
David Brown wrote:> On 18/09/18 04:24, Les Cargill wrote: >> David Brown wrote: >>> On 16/09/18 15:33, Tom Gardner wrote: >>>> On 16/09/18 14:00, David Brown wrote: >> <snip> >>> >>> There are few cases where formal proofs are worth the time and costs >>> involved. But I like - when possible - to write my code with a view >>> that a formal proof /could/ be made if someone were to go to the >>> effort. It is rare that you could prove a whole program - but not >>> uncommon that you could (if you wanted to) prove many of the functions >>> involved. Thinking in terms of pre-conditions, invariants, >>> post-conditions, variants, specifications - that is all good stuff for >>> writing solid code, even if you don't do so formally. >>> >> >> If you stick to something akin to the Haskell Actor model and everything >> is an event, it's not too onerous to use combinators to generate a >> significant subset of all messages. With the proper level of >> introspection, you can "prove" the program works to a limit >> enumerated by the test vectors and that it continues to do so as >> changes are made to the code base. >> > > Testing can /never/ prove a program is correct - unless you can > enumerate /all/ inputs and states of your code and go through them all. > Testing can prove a program is wrong (and it is vital for that), but it > cannot prove a program is correct. >So what you can to is find the meat of what is possible and do that. I must say - I am rather tired of this old warhorse; an appeal to Godel in the form of an economics question. All I would say is that you should test as well as you can. You should use a dragon to fight the dragon. And so if your system is adept at rejecting inputs it cannot expect, then what? It's all about the ability to enforce constraints. Sort your constraints by the ability to do damage.> A functional programming language like Haskell gives you a much better > chance of actually proving the correctness of your code than an > imperative language like C - that is one of the reasons for the > existence of functional programming languages (it is the lack of state > and side-effects that help). But if you want to prove the correctness > of your Haskell program, you do it by an analysis of the code, or by > deriving correct code in the first place - you don't do it by testing. >That's because we'd like to pretend that "analysis" is some process that's not automatable. Or, at least, not somehow aided by automation. I only invoked Haskell because it's the source of the actor pattern.>> The test vectors and captured output can be controlled and >> compared to. And if you want to go as far as model >> checking or partial model checking, you have the stuff in place to >> enforce that now. >> >> >> Obviously, there are domains where you just can't get close enough to >> this ideal. So you gamble. >> > > Indeed - and almost all practical situations fall into this category. >Yeah, I dunno. I think people give up too early.>> <snip> >> >>> >>> Certainly I do not think C is the best choice of language for many of >>> the types of use it is put to. I think most people who program in C >>> would be more productive and write more correct code in other >>> languages - and most programs that are written in C would be better >>> written in other languages. >>> >> >> Possibly. But what C offers is the ability to build nonstandard, hybrid >> "furniture" to support the development effort that can not be >> forseen by language and library designers. This is especially pronounced >> in serialization and the ability to dynamically configure a program ( >> which are two sides of the same coin ). >> > > I don't follow that at all. >So write a C++ thing to dump all the state in Any Random C++ object to a text file. You can get close. A C struct? Gimme thirty minutes and the source code.>> C also supports event-driven-ness in a way that few other languages do. >> > > And I follow that even less. >And that's fine. I accept the following premises: - Model checking is the current state of the art in correctness. - Models don't work without events. - Models work better when they're introspected. - Because C can "cheat" and use the physical representation of objects in memory, it has a small leg up in the game of introspection. C has select()/poll()/epoll() and Real(tm) callbacks.> (I am not saying I disagree with you, I just can't see what you are > trying to say. Maybe I'll understand it better after some coffee.) >For what it is worth, If I knew what I was trying to way, I'd say it :)> C certainly has its important features and strengths, and is a very > useful language to have. >So the tack I've taken is to cobble together things that make C do what I want it to ( with a scripting language adept at string processing ) rather than wait on someone else to provide things for me. -- Les Cargill
Reply by ●September 22, 20182018-09-22
Tom Gardner wrote:> On 18/09/18 03:24, Les Cargill wrote: >> David Brown wrote: >>> On 16/09/18 15:33, Tom Gardner wrote: >>>> On 16/09/18 14:00, David Brown wrote: >> <snip> >>> >>> There are few cases where formal proofs are worth the time and costs >>> involved. But I like - when possible - to write my code with a view >>> that a formal proof /could/ be made if someone were to go to the >>> effort. It is rare that you could prove a whole program - but not >>> uncommon that you could (if you wanted to) prove many of the >>> functions involved. Thinking in terms of pre-conditions, invariants, >>> post-conditions, variants, specifications - that is all good stuff >>> for writing solid code, even if you don't do so formally. >>> >> >> If you stick to something akin to the Haskell Actor model and >> everything is an event, it's not too onerous to use combinators to >> generate a significant subset of all messages. With the proper level >> of introspection, you can "prove" the program works to a limit >> enumerated by the test vectors and that it continues to do so as >> changes are made to the code base. >> >> The test vectors and captured output can be controlled and >> compared to. And if you want to go as far as model >> checking or partial model checking, you have the stuff in place to >> enforce that now. > > That's nothing to do with formal proofs, of course. >Yes. Of course. It is, as all good engineering is, about the retirement of risk.> It is equivalent to "inspecting quality into a product". >Oh heck no. Try "introspecting quality into a product". -- Les Cargill
