The best we can do is write simple, understandable code with as few indirections and as little undocumented magic as possible.
Applies very well to all programming.
I was mostly C developer (80% C, 20% C++) for 4 years in a big project (I was backend developer of ICQ Instant Messenger). It has more than 2M lines of C code. Almost all libraries was written from scratch in C language (since ICQ is very old project, many of essential stuff was written within AOL).
I felt comfortable to write high level code in C.
When I read Nginx source code (it's written in C), I see better code quality than 90% of proprietary commercial software which is written on nice and comfortable high level languages.
Good developer is able to write high quality code in C language with minimum bugs in large scale project. Regardless of how nice and high level and convenient language, bad developer will write c....y code.
You can also check my personal project which is written entirely in C. (I didn't contribute for 1.5 years to my github since I was changed countries of living, jobs etc. I hope I will return to it when my life become stable again).
P.S. To be clear, I think that C++11 is great language. But unlike many C++ developers, I love pure C.
The people and the culture/organization of the shop counts for much more than your language. Language counts for something, but it's not where you get the most bang for your buck, and it shouldn't be your first priority!
That said you can create message-passing systems in either - Objective-C was originally a C library and cross-compiler.
Every professional security researcher reading this just raised an eyebrow and thought to themselves, "That's a vulnerable application." In fact, your team (or a similar one at AOL) did introduce vulnerabilities[1][2]. If we assume that, as you imply, AOL really was exclusively composed of above average C developers writing high quality code, this should really just demonstrate the point for us.
I'm sure your team wrote high quality C code (or at the very least, tried very hard to write high quality C code), and as someone who likes C I also dislike the meme that C should simply not be written, no exceptions. I'd probably change it to, "Don't write C unless you need extreme performance, have great engineering resources and you'll generate unmitigated financial returns such to make any reasonable business risk assessment moot." That means virtually the same thing for anyone reading it, but it sounds a lot less sexy and memorable as far as programming aphorisms go.
I have never professionally audited a C project and not found a vulnerability. Most of my friends in this industry would likely say the same. I've never seen a serious audit of a "large" (100kloc or more) C project by a serious, reputable firm with no vulnerabilities reported. If you wrote 2 million lines of C code, if you wrote libraries from scratch, you have serious vulnerabilities. Otherwise, your engineering practices and resources exceed NASA's in formal verification and correctness.
I believe it is theoretically possible to write 100% safe C code, for some approximation of that ideal that leaves aside the ivory tower definition ("the only safe machine is the one which is off"). But I also believe this is so expensive and resource intensive (secure coding standards, audits, attempts at formal verification and provable correctness) that it's just generally not realistic in practice.
The reason I am saying all of this is not to attack you or your sense of worth as a C developer. Rather, I'd like you to consider that you simply have no idea how many vulnerabilities exist in ICQ. In fact, I found eight different security reports for ICQ, linked at the bottom. One of the more serious ones allowed arbitrary email retrieval, which I'm willing to bet was introduced because your team liked to develop in-house libraries and decided to do that for POP3.
C is a language which is both very powerful and which requires constant vigilance while coding. It is a language which makes pushing a buffer overflow to production on a Friday at 3 pm very easy. I bet your team was comparatively well-versed in C vulnerabilities for the time, but the very fact that you rolled libraries from scratch tells me you already have a high probability of errors showing up. Rolling a library/framework in-house is basically the first thing security researchers look for in an audit, because the third party ones are (usually) more secure due to their exposure. When you further consider the probability of third party software you did use becoming vulnerable in the future, changing compiler optimizations introducing new vulnerabilities and the sheer size of the SEI CERT Secure Coding Standard itself, you are left with a very dangerous risk profile.
We cannot expect C to be a safe language for general use if you need to have the rigor of one of the best research organizations in the world coupled with the top 0.01% of all C programmers. It just isn't feasible.
[1]: http://www.coresecurity.com/content/bevy-of-new-icq-vulnerab...
[2]: https://www.cvedetails.com/vulnerability-list/vendor_id-123/...
> Every professional security researcher reading this just raised an eyebrow and thought to themselves, "That's a vulnerable application."
That may be true, but substitute "C" with "Python" and wouldn't you have the same reaction? Maybe you would expect it to be slightly less vulnerable, but the key risk that I read in that statement (I am not a security professional) is the "2M" and the "written from scratch". The risk from "C" is secondary.
I think the reason why every seasoned security researcher I've met also happens to be a heavy drinker or is damaged in some way is because they're in a war of attrition. You want perfect security but it will never happen. These are ultimately mutating, register-based machines. We will probably never be certain that with a sufficient level abstraction a program can be written which will never execute an invalid instruction or be manipulated to reveal hidden information.
Where the theory hits the road is where the action happens.
Which is how we end up with this wide spectrum of acceptable tolerances to security. Holistic verification of systems is extremely costly but necessary where human lives matter. However if someone finds a weird side-channel attack in a bitmap parsing library I think we can be more forgiving.
The whole idea that C programs are insecure by default and can never be secure is where theory wants to ignore the harsh realities. We can write languages with tighter constraints on the verification of the programs they create which will lower the risk of most security exploits by huge margins... but we have to trade something away for the benefit. The immediate costs being run-time performance or qualitative things like maintainability.
What I ultimately think will make these poor security researchers feel better is liability. Having a real system and standard in place for professional practices will at least let us soak up the damage will force us to consider security and scrutinize our code.
There are all kinds of people doing security research. In my experience with some of those people that I've met it doesn't seem like the challenges they have to contend with are not unrelated to the stress caused by the work that they do.
Sort of like how someone who works with giant metal stamping presses is likely to be missing a couple of fingers if they've worked long enough with them (and in an environment where safety regulations are too relaxed).
These are also some of the wonderful people in my life and I enjoy them very much.
But you have to take care of yourself!
They are not proven to be safe, they are proven to adhere to whatever the proof system managed to prove. This shifts the possible vulnerabilities away from the actual code and onto the proof system and the assumptions that the proof system makes.
For example, take a C program that was proven to be absolutely free of buffer overflows. And therefore labelled by the proof system as 'secure'. But, unbeknownst to the proof system, the C program also interprets user-supplied input as a format string! So it's still vulnerable to format string exploits.
Correct proof systems probably add a huge margin of security compared with the current security standards, but it's not absolute.
I think C++ can only get so far, without deprecating some of C. Or at least C style code, should come with a big warning from the compiler:
"You are using an unsafe language feature. Are you absolutely sure there is no bug here, and there are no way to use safe language features instead?"
In libraries there might be cases where C-style code like manual pointer arithmetic, c arrays, manual memory management, c-style casts, or *void pointers, uninitialized variables, etc are necessary. But in user code most often there are safer replacements.
No, it doesn't succeed at this at all. Large C++ codebases routinely suffer from the same problems that C does.
For proof, search the CVE lists for browser vulnerabilities.
I don't think that's true. There's no reason why memory safety has to cost either performance or maintainability.
It feels like there's some sort of fundamental dichotomy because we didn't know how to do it in 1980, and we're still using languages from 1980, but our knowledge has advanced since then.
This is the wrong mindset and has been the guiding principle behind over a generation of poor programming discipline.
You might be able to rationalize that you don't always need extreme performance, but it's not about performance, it's about efficiency. Efficiency always matters. We live on a small planet with finite resources. Today, the majority of computing is happening with handheld portable devices with tiny batteries. Every wasted byte and CPU cycle costs power, runtime, and usability.
Even if you're coding for a desktop PC or a server application - every bit of waste costs electricity, generates heat, increases cooling load. Every bit of waste costs the user real money, even if they don't see the time that you wasted for them.
Performance is a side-effect. The only thing that matters is efficiency, and it matters all the time.
Most of today's programming problems come down to laziness and fear of "premature optimization" (which is obviously bunk). It is possible to write perfect C code that runs correctly the first time and every time. You do that by planning ahead. Formal specs are part of this.
The same consideration applies to writing, in general. I witnessed this first hand, when I worked at the computer labs at the University of Michigan back in the 1980s. When all anyone had was an electric typewriter, they planned their papers out well in advance - detailed outlines, with logically designed introductions and conclusions. This was a requirement, because once you got into actually typing, correcting a mistake could be expensive or impossible without starting over from scratch.
When we only had Wordstar available, and users came in with the inevitable questions and requests for help, you would still see well-organized papers written with a clear logical flow.
In 1985 with the advent of the Macintosh and MacWrite, all of that changed: People discovered that they could edit at will, copy and paste and move text around on the fly. And so they did - throwing planning out the window. And the quality of papers we saw at the help desk plummeted. Surveys from those years confirmed it too - paradoxically, the writing scores in the better-funded departments dropped rapidly, commensurate with their rate of introduction of Macs.
Planning ahead, making sure you know what you need to write, before you start writing any actual lines of code, prevents most problems from ever happening. It's a pretty simple discipline, but one that's lost on most people today.
If "planning ahead" were enough to prevent security vulnerabilities in practice, someone would have done it by now. Instead, we've had C for upwards of 30 years and everyone, "bad programmers", "good programmers" and "10xers" alike, keeps introducing the same vulnerabilities.
It's a nice theory, but we've been trying for over 30 years to make it work, and it keeps failing again and again. I think it's time to admit that C as a secure language (modulo the extremely expensive formal coding practices used in avionics and whatnot) has failed.
Security is not a property of the tool, it is a property of the tool's wielder.
How many memory safety bugs do you see in Java applications compared to C applications?
Writing in Java is an effective way to reduce remote code execution vulnerabilities over writing in C. Statistics have shown this over and over again.
Remote code execution vulnerabilities in C are less a feature of the language syntax and mostly due to the abysmally poor C library, which is regrettably part of "C The Language" - but no one forces you to use it - there are better libraries. Also, it's an artifact of implementation - just as Java's supposed immunity is an artifact of implementation, not an inherent feature of the language syntax.
Case in point http://www.trendmicro.com/vinfo/us/threat-encyclopedia/vulne...
As for RCEs in C code - these would be easily avoided if the implementation used two separate stacks - one for function parameters, and one for return addresses. If user code can only overwrite passive data, stack smashing attacks would be totally ineffective. Again - there's nothing in the C language specification that dictates or defines this particular vulnerability. It is solely an internal implementation decision.
No. Increasingly, RCEs are due to vtable confusion resulting from use after free.
Meanwhile, new programming languages abound, presumably to make programmers' lives easier. But these developments often completely lose sight of the users. Python is easier to write, but a program written in python uses 1000x the CPU and memory resources of a program written in C. It does the job, but slowly, and consuming so much that the computer is unable to do anything else productive. Meanwhile, it's questionable whether programmers' lives have been improved either, because they spend too much time chasing the next new tool instead of growing expertise in just one.
As for marginal efficiency gains - that is only a symptom of the latter developer problem. E.g., LMDB is pure C, less than 8KLOCs, and is orders of magnitude faster than every other embedded database engine out there. It is also 100% crash-proof and offers a plethora of features that other DB engines lack. All while being able to execute entirely within a CPU's L1 cache. The difference is more than "marginal" - and that difference comes from years of practice with C. You will never gain that kind of experience by being a dilettante and messing with the flavor of the week.
Just out of interest: How many C projects have you audited? And have you ever looked for a relationship between the number of vulnerabilities and the percentage code coverage from automated tests?
But how is that a useful or replicable result, that will work in the real world for other projects? You're basically saying that everyone just needs to be a top 0.001% C programmer. This is the "abstinence-only sex education" of programming advice. It's super simple to not get STDs or have out-of-wedlock pregnancies - just don't have sex with anyone but your spouse, and ensure they do the same. It's 100% guaranteed to work, and if you don't follow that advice you're stupid and deserve whatever bad things happen to you.
For the record, I don't think your stupid if you have a child accidentally.
However, once you do accidentally have a child, the results are often not pretty, and I will feel bad watching as you deal with the consequences of your poorly thought out decision.
Regarding programming, I can't see the relationship you make at all.
If you write a good program, well good job. If you write a bad program, you are probably going to write a better one next time. (Ever look back at your old code?)
It takes practice to get good, and the more we work at it, the better we'll get. Just keep trying.
It's as if I say: "Step 1 of writing good code: Don't make mistakes. If you make mistakes, you deserve what's coming to you!" Some mistakes are expected, and essentially inevitable; they're the default, not the exception. Blaming the programmer might seem like the right thing to do, but there's more practical benefit to improving the tools and teaching programmers how to handle errors, so that we can decrease the negative impact that bugs will have.
I have two words for you: MAINTENANCE PROGRAMER.
Now that I think of it, there's another parallel with unwanted pregnancies. There are men that stick around, and there are boys who run and let others clean up after their mess.
What is this, 1953?
There are a great number of couples choosing to have children in stable, committed - yet unmarried - relationships.
The comment struck me as incredibly anachronistic, bordering on offensively so.
please don't.
Way to hijack a useless subthread and do something useful with it. Great meta-point. Honestly. This feature alone makes the comments on Reddit bearable for consumption.
Should be 1967.
</s>
I imagine that this poster and his team took a similar approach with C: avoiding the dangerous features, or just finding ways to factor them out.
A more constructive/charitable phrasing of the parent's point might be: you should only be allowed to code in C if you're already a top 0.001% programmer. Then, obviously, all C code will be good—not that there'll be much of it.
That's actually a more interesting point than it seems. Programmers generally tend to reject the idea of guilds and "professional" licensing—mostly because, AFAIK, most programs aren't critical and most crashes don't matter. But what if, instead of licensing all programming, we just licensed only low-level programming? What if, as a rule, everyone who was going to be hired to write code in a language with pointers was union-mandated to be certified as knowing how to safely fiddle with pointers? That could probably split on interesting dimensions, like a bunch of regular coders working in e.g. a Rust codebase, with a certified Low Level Programmer needing to "sign off on" any commit that contained unsafe{} code, where the actual failure of the unsafe{} code would get the Low Level Programmer disbarred.
I'm a very experienced C programmer and one day my boss came to me and said that the sales guys had already sold a non-existing client side module to a house hold name appliance manufacturer. The deal was inked and it had to be ready in only 3 months. Even worse, it had to run in the Unix kernel of the appliance and therefore be rock solid so as to not take the whole appliance down. It also had to be ultra high performance because the appliance was ultra high performance and very expensive. Now the really bad news: I had a team made up of 3 more experienced C developers (including myself) and 3 very un-experienced C developers. We also estimated that in order to code all the functionality it would take at least 4 months. So we added on another 4 less experienced C developers (the office didn't have a lot of C developers). The project was completed in time, a success, and almost no bugs were found, and yet many developers without much C experience worked on the project. How?
(a) No dynamic memory allocation was used at run-time and therefore we never had to worry about memory leaks.
(b) Very, very few pointers were used. Instead mainly arrays. And not just C developers understand array syntax, e.g. myarray[i].member = 1 :-) Therefore we never had to worry about invalid pointers.
(c) Source changes could only be committed together with automated tests resulting in 100% code coverage and after peer review. This meant that most bugs were discovered immediately after being created but before being checked in to the source repository. We achieved 100% code coverage with an approx. 1:1 ratio of production C source code to test C source code.
(d) All code was written using pair programming.
(e) Automated performance tests were ran on each code commit to immediately spot any new code causing a performance problem.
(f) All code was written from scratch to C89 standards for embedding in the kernel. About a dozen interface functions were identified which allowed us to develop the code in isolation from the appliance, and not have to learn the appliance etc.
(g) There was a debug version of the code littered with assert()s and very verbose logging. Therefore, we never needed to use a traditional debugger. The verbose logging allowed us to debug the multi-core code. Regular developers were not allowed to use mutexes etc themselves in source code. Instead, generic higher level constructs were used to achieve multi-core. My impression is that debugging via sophisticated log files is faster than using a debugger.
(h) We automated the process of the Makefile so that developers could create new source files and/or libraries on-the-fly without having to understand make voodoo. C header files were also auto generated to increase developer productivity.
(i) Naming conventions for folders, files, and C source code were enforced programmatically and by reviews. In this way it was easier for developers to name things and comprehend the code of others.
In essence, we created a kind of 'dumbed down' version of C which was approaching being as easy to code in as a high level scripting language. Developers found themselves empowered to write a lot of code very quickly because they could rely on the automated testing to ensure that they hadn't inadvertently broken something, even other parts of the code that they had little idea about. This only worked well because there was a clear architecture and code skeleton. The rest was like 'painting by numbers' for the majority of developers who had little experience with C.
The same team went on to develop more C software using the same technique and with great success.
Unfortunely your case is the exception that confirms the rule.
I never saw a company using C like that.
On my case the teams used to be composed from circa 30 developers, scattered around multiple consulting companies with high attrition.
Another tidbit: The developer pairs were responsible for writing both the production code and associated automated tests for the production code. We had no 'QA' / test developers. All code would be reviewed by a third developer prior to check-in. However, at one stage we tried developing all the test code in a high level scripting language with the idea that it would be faster to write the tests and need less lines of test source code. However, because we did several projects like this, we noticed that there was no advantage to writing tests in a scripting language. The ratio of production C source lines to test source lines was about the same whether the test source code was written in C or a scripting language. Further, there was an advantage to writing the tests in C because they ran much faster. We had some tens of thousands of tests and all of them could compile and run in under two minutes total, and that includes compiling three version of the sources and running the tests on each one; production, debug, and code coverage builds. Because the entire test cycle was so fast then developers could do 'merciless refactoring'.
Which is to say, your story matches my hypothetical pretty well. You effectively created the same structure as Rust has, where there are safe and unsafe sublanguages, and the "master" developers thoroughly audited any code implemented in the unsafe sublanguage.
Which makes my point: there exist a small set of people qualified to write in "full C", and a much-larger set of people who aren't; and the only way—if you're a person who isn't qualified—to write C that doesn't fall down, is with the guidance and leadership of a person who is.
Though I think maybe your thesis statement agrees with that, so maybe I'm not arguing with you. Not all the developers on a given project need to be from the qualified set, no. But at least some of the developers need to be from the qualified set, and the other developers need to consider the qualified ones' guidance—especially on what C features to use or avoid—to be law for the project. As long as they stay within those guidelines, they're really working within a DSL the "master" developers constructed, not in C. And nobody ever said you can't make an idiot-proof DSL on top of C; just that, if you need everything C offers, your the only good option is to remove the idiots. :)
I also forgot to mention about performance. Whether you code * foo or the easier to comprehend and safer(?) foo[i] then the compiler still does an awesome job optimizing. However, it's much easier to assert() if variable i is in range rather than *foo. And it's also easier to read a verbose log variable i (usually a 'human-readable' integer) than to read a verbose log pointer (a 'non-human-readable' long hex number). At the time we wrote a lot of network daemons for the cloud and performance tested against other freely available code to ensure that we weren't just re-inventing the wheel. NGINX seemed to be the next fastest, but our 'dumbed down' version of C ran about twice as fast as NGINX according to various benchmarks at the time. Looking back, I think that's because we performance tested our code from the first lines of production code, and there was no chance for any type of even puppy fat to creep in. Think: 'Look after the cents and the dollars look after themselves' :-) Plus NGINX also has to handle the generic case, whereas we only needed to handle a specific subset of HTTP / HTTPS.
I wanted to interpret it as you shouldn't write code if you can avoid it.
I'm certain that's not what he meant, but it sounds better.
Good developer is able to write high quality code in C...
- Was your code unit-tested?
- Did you use the 'strn' functions? (strncpy, instead of strcpy for example)
- Did your code run under Valgrind? (was there valgrind at that time? I'm not sure)
- Was it tested for memory leaks?
- Was there input fuzzying tests?
I agree that there are ways of writing great C code (like nginx, the linux and BSD kernels, etc)
But from a certain point on you're just wasting developer time when you would have a better solution in Java/Python/Ruby, etc with much less developer time and much less chance of bugs and security issues.
There was not one unit test. And there probably still isn't.
Why wouldn't you unit test in C? I do and I have found lot's of bugs as a result and maintaining code is much easier.
1. write a new one file script which parses function declarations from a source code file
2. have the script find all function declarations which start with "utest_", accept no parameters, and return "int" or "bool".
3. have the script write out a new C file which calls all of matching unit test functions and asserts their return value is equal to 1
4. have your Makefile build and run a unit test binary using code generated by your script for each source code file containing greater than 0 unit tests.
Writing a script to parse function declarations from your C source code is useful because you can extend the script later on to generate documentation, code statistics, or conduct project-specific static analysis.
https://randomascii.wordpress.com/2013/04/03/stop-using-strn...
But if you're using C++, use C++ strings, you don't need strcpy
There's strlcpy mentioned there, which seems a better C solution
I interpreted that differently than you. I didn't think take it to use another language. But to keep c code as concise as possible and to not reinvent the wheel when a good library is available.
I have seen the quite a few of those and I imagine you wouldn't enjoy to audite their code.
A good programmer will make COBOL look clean and understandable. But on average, I could way C code requires a lot more discipline, knowledge, and experience to produce quality code.
* You've never deployed one.
* You've never had to maintain one.
* You wrote the last line of code and handed it over to the maintenance team, who then never gave you feedback.
* You have no customers.
* You have done a never-before-seen formal analysis of a large scale project down to the individual source line level, and made no mistakes with the formal specification.
The author is correct: use C only if you must. There are still an enormous number of reasons why you must use C, but it should be a constraint imposed on you, and not a language you actively want to start a project in.
It's the same as with, say, goto or #ifdef's - one has to consider the alternatives and make an informed choice. Most of the time, the alternatives are preferable, but sometimes there either aren't any alternatives, or they are even worse.
Which is not to say that C can't be a whole lot of fun. I love it dearly. But I, too, tend to avoid it when I can. It's just too easy to shoot yourself in the foot.
(of course, one employer appropriately used C as a portable assembler, and respected it as such, for the purposes of developing a cross compiler and tool emulations for an older minicomputer environment; the next was doing (batch) "business applications" and foolishly spent too little on hardware and too much wasted effort on application development)
Pascal (Modula) did much the same, SAFELY, but the money wasn't put into compiler optimization :-(
Interesting that the GNU compiler collection now includes a very efficient Ada compiler.
GNAT has existed for ... at least ten years, I think. The DOD apparently paid for the development so there would be at least one open source/free software implementation. (According to Wikipedia, development started about twenty years ago, and it was merged into GCC in 2001.)
Parent seems to believe in nginx. But as a guy who actually tried to do a few of those things with nginx I can confirm that nginx's code base is pretty awful and working around all the usual pitfalls of C in nginx is a huge PITA and enormous amount of work.
(same username on github)
I like tweaking younger engineers with C eccentricities, but any commercial code tends towards being as vanilla as possible with lots of error checking and docs to be as clear as possible.
1. Almost devoid of any documentation. 2. No ADTs - all struct fields are directly accessed, even though there are sometimes very complicated invariants that must be preserved (and these invariants are not documented anywhere, of course). 3. Ultra-short variable names that really describe nothing but their types (it's like Hungarian notation with only the notation part). 4. These mystery variables are all defined in the top of the function of course, making them hard to trace. Does anyone even compile Nginx with C89? 5. Configuration parsing creates a lengthy boilerplate that's really hard to track. 6. Asynchronous code is very hard to track, with a myriad of phase-specific meaning for return codes, callbacks and other stuff that makes reading Boost.ASIO code look like a walk in the park.
I think it really shows the sad state of C programming. Die-hard C programmers always complain C++ is hard to read because of its template and OOP abstractions, and it sometimes really is a mess to read, but C is even harder since large programs always re-implement their own half-assed version of OOP and template-macros inside.
You meant "one of the worst"?
None of which removes the need to write simple, understandable code without undocumented magic. But we should not be throwing up our hands and treating invalid accesses, memory safety failures, buffer overflows, SQL injection, XSS, or a whole host of common failures as inevitable. It really is possible to do a lot better than most programs and a lot better than C.
Provable correctness "...has not been tried and found wanting; it has been found difficult and not tried."
We're writing programs that are tens of millions of lines of code (OSes, databases, air traffic control systems). My impression of provable correctness is that the largest program that has been proven is in the area of 100,000 lines (feel free to correct if I am in error). We need to be able to prove programs two orders of magnitude bigger than that; provable correctness has not been tried for such programs because nobody wants to wait a generation or two before they get the results.
They key is then to simply avoid emergent interactions between modules/subsystems. That's pretty doable.
What doesn't happen is that people never reason about the cost of defects. Even if they do some reasoning about this, they don't apply that to other components of systems.
You code in a functional style and/or with state machines composed. They composed stuff hierarchically and loopfree where possible to facilitate analysis. Each component is small enough to analyze for all success or failure states. The results of each become "verification conditions" for things that build on it. With such methods, one can build things that are as large as you want so long as each component (primitive or composite) can be analyzed.
Not clear at what point this breaks down. I used it for drivers, protocols, algorithms, systems, networks, and so one. I brute forced it with more manual analysis because Im not mathematical or trained enough for proofs. However, what holds it back on large things is usually just lack of effort far as I can tell.
How many modern programmers hold this mistaken belief? It's false -- the Turing Halting problem (https://en.wikipedia.org/wiki/Halting_problem) demonstrates that one cannot establish that a non-trivial program is "provably correct."
It seems the OP got carried away with his rhetoric, and the way he put it is simply wrong.
The halting problem says that there exist programs that cannot be proven correct; it says that for any property you want to prove computationally, no program can give you an answer for every last program. It doesn't say anything about "non-trivial" programs. In particular, if you write programs with awareness of the halting problem in mind, you can write extremely complicated programs that are provably correct.
One straightforward way to do this is with a language that always halts. The proof assistant Coq is based on such a language, and it's powerful enough to write a C compiler: http://compcert.inria.fr/
It is certainly correct that you can't stuff an arbitrarily vexatious program through a proof assistant and get anything useful on the other side. But nobody is interested in proving things about arbitrarily vexatious programs; they're interested in proving things about programs that cooperate with the proof process. If your program doesn't want to cooperate, you don't need an exact answer; you might as well just say "No, I don't care, I'm not trusting you."
The way you prove halting is to find some integer measure for each loop (like "iterations remaining" or "error being reduced") which decreases on each iteration but does not go negative. If you can't find such a measure, your program is probably broken. (See page 12 of [1], the MEASURE statement, for a system I built 30 years ago which did this.)
The measure has to be an integer, not a real number, to avoid Zeno's paradox type problems. (1, 1/2, 1/4, 1/8, 1/16 ...)
On some floating point problems, with algorithms that are supposed to converge, proving termination can be tough. You can always add an iteration counter and limit the number of iterations. Now you can show termination.
Microsoft's Static Driver Verifier is able to prove correctness, in the sense of "not doing anything that will crash the kernel", about 96% of the time. About 4% of the time, it gives up after running for a while. If your kernel driver is anywhere near close to undecidability, there's something seriously wrong with it.
In practice, this is not one of the more difficult areas in program verification.
[1] http://www.animats.com/papers/verifier/verifiermanual.pdf
No, but its source does. The source for the Turing Halting problem is Gödel's incompleteness theorems, which do specify that the entities to which it applies are non-trivial. The Turing Halting problem, and Gödel's incompleteness theorems, are deeply connected.
> One straightforward way to do this is with a language that always halts.
That doesn't avoid the halting problem, it only changes the reason for a halt. And it cannot guarantee that that program will (or won't) halt, if you follow -- only its interpreter.
> In particular, if you write programs with awareness of the halting problem in mind, you can write extremely complicated programs that are provably correct.
You need to review the Turing Halting problem. No non-trivial computer program can be proven correct -- that's the meaning of the problem. It cannot be waved away, any more than Gödel's incompleteness theorems can be waved away, and for the same reason.
Gödel doesn't say anything about "non-trivial" any more than Turing does. His first theorem is a "there exists at least one statement" thing, just like the halting problem. Like the halting problem, the proof is a proof by construction, but that statement is not a statement that anyone would a priori are to prove, just like the program "If I halt, run forever" is not a program that anyone would particularly want to run. So while yes, they're deeply connected, from the point of view of proving actual systems correct, it's not clear they matter. And neither theorem says anything about "non-trivial" statements/programs (just about non-trivial formalizations and languages).
Gödel's second theorem is super relevant, though: it says that any consistent system cannot prove its own consistency. But that's fine. Coq itself is implemented in a Turing-complete language (ML), not in Coq. It would be nice if we could verify Coq in Coq itself, but since Gödel said we can't, we move on with life, and we just verify other things besides proof assistants. (And it seems to be worthwhile to prove things correct in a proof assistant, even without a computer-checked proof of that proof assistant's own correctness.)
This is not waving away the problem, it's acknowledging it and working within the limits of the problem to do as much as possible. And while that's not everything, it turns out a lot of stuff of practical importance -- perhaps everything of practical importance besides proving the system complete in its own language -- is possible.
Source: https://en.wikipedia.org/wiki/Halting_problem
Quote: "Rice's theorem generalizes the theorem that the halting problem is unsolvable. It states that for any non-trivial property, there is no general decision procedure that, for all programs, decides whether the partial function implemented by the input program has that property. (A partial function is a function which may not always produce a result, and so is used to model programs, which can either produce results or fail to halt.) For example, the property "halt for the input 0" is undecidable. Here, "non-trivial" means that the set of partial functions that satisfy the property is neither the empty set nor the set of all partial functions."
Source: https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...
Quote: "Gödel's incompleteness theorems are two theorems of mathematical logic that establish inherent limitations of all but the most trivial axiomatic systems capable of doing arithmetic."
> It would be nice if we could verify Coq in Coq itself ...
I was planning to bring this issue up, but you've done it for me. The simplest explanation of these two related theorems involves the issue of self-reference. Imagine there is a library, and a very conscientious librarian wants to have a provably correct account of the library's contents. The librarian therefore compiles an index of all the works in the library and declares victory. Then Gödel shows up and says, "On which shelf shall we put the index?"
In the same way, and for the same reason, non-trivial logical systems cannot check themselves, computer languages cannot validate their products (or themselves), and compilers cannot prove their own results correct.
> And it seems to be worthwhile to prove things correct in a proof assistant, even without a computer-checked proof of that proof assistant's own correctness.
Yes, unless someone is misled into thinking this means the checked code has been proven correct.
> This is not waving away the problem ...
When someone declares that a piece of code has been proven correct, in point of fact, yes, it is.
> all but the most trivial axiomatic systems
This is about non-trivial properties on arbitrary programs, and non-trivial axiomatic systems proving arbitrary statements. It is not about non-trivial programs or non-trivial statements.
Rice's theorem states that, for all non-trivial properties P, there exists a program S where you cannot compute P(S). (The Wikipedia phrasing puts the negative in a different spot, but this is de Morgan's law for quantifiers: ∀P ¬∀S P(S) is computable = ∀P ∃S ¬ P(S) is computable.)
Gödel's first theorem is that, for all non-trivial formalizations P, there exists a statement S where you cannot prove P in S.
You are claiming, for all non-trivial properties P, for all non-trivial programs S, you cannot compute P(S); for all non-trivial formalizations P, for all non-trivial statements S, you cannot prove P in S.
This is not what Rice's or Gödel's theorems are, and not what the texts you quoted say.
> Then Gödel shows up and says, "On which shelf shall we put the index?"
You keep it outside the library. The index tells you where every single book is, other than the index.
In particular, Gödel claims that, if the index has any chance of being correct, it must be outside the library. The fact that Coq cannot be proven in Coq does not decrease our confidence that it is correct; in fact, Gödel's second theorem means that if it could be proven in itself, we'd be confident it was wrong!
> You keep it outside the library. The index tells you where every single book is, other than the index.
This approach would have saved Russell and Whitehead's "Principia Mathematica" project, would have placed mathematics on a firm foundation, but it suffers from the same defect of self-reference -- it places the index beyond validation. Russell realized this, and recognized that Gödel's results invalidated his project.
> The fact that Coq cannot be proven in Coq does not decrease our confidence that it is correct;
Yes, true, but for the reason that we have no such confidence (and can have no such confidence). We cannot make that assumption, because the Turing Halting problem and its theoretical basis prevents it.
Source: http://www.sscc.edu/home/jdavidso/math/goedel.html
Quote: "Gödel hammered the final nail home by being able to demonstrate that any consistent system of axioms would contain theorems which could not be proven. Even if new axioms were created to handle these situations this would, of necessity, create new theorems which could not be proven. There's just no way to beat the system. Thus he not only demolished the basis for Russell and Whitehead's work--that all mathematical theorems can be proven with a consistent set of axioms--but he also showed that no such system could be created." (emphasis added)
One particular project. The specific project of formalizing mathematics within itself is unachievable. That doesn't mean we've stopped doing math.
And this is in fact the approach modern mathematics has taken. The fact that one particular book (the proof of mathematics' own consistency) can't be found on the shelves doesn't mean there isn't value in keeping the rest of the books well-organized.
> Yes, true, but for the reason that we have no such confidence (and can have no such confidence). We cannot make that assumption, because the Turing Halting problem and its theoretical basis prevents it.
No! Humans aren't developed in either Coq or ML. A human can look at Coq and say "Yes, this is correct" or "No, this is wrong" just fine, without running afoul of the halting problem, Gödel's incompleteness theorem, or anything else. The fact that you can have no Coq-proven confidence in Coq's correctness does not mean that you can have no confidence of Coq's correctness.
(Of course, this brings up whether a human should be confident in their own judgments, but that's a completely unavoidable problem and rapidly moving to the realm of philosophy. If you are arguing that a human should not believe anything they can convince themselves of, well, okay, but I'm not sure how you plan to live life.)
This is like claiming that, because ZF isn't provably correct in ZF (which was what Russell, Whitehead, Gödel, etc. were concerned about -- not software engineering), mathematicians have no business claiming they proved anything. Of course they've proven things just fine if they're able to convince other human mathematicians that they've proven things.
> One particular project.
A mathematical proof applies to all cases, not just one. Gödel's result addressed Russell's project, but it applies universally, as do all valid mathematical results. Many mathematicians regard Gödel's result as the most important mathematical finding of the 20th century.
> That doesn't mean we've stopped doing math.
Not the topic.
> A human can look at Coq and say "Yes, this is correct" or "No, this is wrong" just fine, without running afoul of the halting problem, Gödel's incompleteness theorem, or anything else.
This is false. If the Halting problem is insoluble, it is also insoluble to a human, and perhaps more so, given our tendency to ignore strictly logical reasoning. It places firm limits on what we can claim to have proven. Surely you aren't asserting that human thought transcends the limits of logic and mathematics?
> Of course they've proven things just fine if they're able to convince other human mathematicians that they've proven things.
Yes, with the caution that the system they're using (and any such system) has well-established limitations as to what can be proven. You may not be aware that some problems have been located that validate Gödel's result by being ... how shall I put this ... provably unprovable. The Turing Halting problem is only one of them, there are others.
Given that both logic and mathematics are creations of human thought, is this really so untenable?
What? I have no idea what you mean by "applies universally" and "all valid mathematical results."
A straightforward reading of that sentence implies that Pythagoras' Theorem is not a "valid mathematical result" because it applies only to right triangles. That can't be what you're saying, is it?
I am acknowledging that Gödel's second theorem states that any mathematical system that attempts to prove itself is doomed to failure. I am also stating that Russell's project involved a mathematical system that attempts to prove itself. Therefore, Gödel's second theorem applies to Russell's project, but it does not necessarily say anything else about other projects.
> Many mathematicians regard Gödel's result as the most important mathematical finding of the 20th century.
So what? This is argumentum ad populum. How important the mathematical finding is is irrelevant to whether it matters to the discussion at hand.
> This is false. If the Halting problem is insoluble, it is also insoluble to a human
OK, so do you believe that modern mathematics is invalid because Russell's project failed?
Obviously, the solution is to stop writing arbitrary programs. As Dijkstra said long ago, we need to find a class of intellectually manageable programs - programs that lend themselves to being analyzed and understood. Intuitively, this is exactly what programmers demand when they ask for “simplicity”. The problem is that most programmers' view of “simplicity” is distorted by their preference for operational reasoning, eschewing more effective and efficient methods for reasoning about programs at scale.
Can you clarify your last sentence? What do you mean by "preference for operational reasoning"? What's an example of the more effective methods for reasoning about programs at scale that you're contrasting this to?
By “more effective methods for reasoning about programs at scale”, what I mean is analyzing the program in its own right, without reference to specific execution traces. There are several kinds of program analyses that can be performed without running the program, but, to the best of my knowledge, all of them are ultimately some form of applied logic.
Not really. It's also possible to reason non-operationally about imperative programs, e.g., using predicate transformer semantics. It's also possible to reason operationally about non-imperative programs.
You're overlooking the issue of self-reference. A given computer language can validate (i.e. prove correct) a subset of itself, but it cannot be relied on to validate itself. A larger, more complex computer language, created to address the above problem, can check the validity of the above smaller language, but not itself, ad infinitum. It's really not that complicated, and the Halting Problem is more fundamental than this entire discussion seems able to acknowledge.
Also, it seems you misunderstand Gödel/Turing/etc.'s result. What a consistent and sufficiently powerful formal system can't do is prove its own consistency as a theorem. Obviously, it isn't sustainable to spend all our time inventing ever more powerful formal systems just to prove the preceding ones consistent. At some point you need to assume something. This is precisely the rôle of the foundations of mathematics (or perhaps I should say a foundation, because there exist many competing ones): to provide a system whose consistency need not be questioned, and on top of which the rest of mathematics can be built.
In any case, we have gone too far away from original point, which is that, if arbitrary programs are too unwieldy to be analyzed, the only way we can hope to ever understand our programs is to limit the class of programs we can write. And this is precisely what (sound) type systems, as well as other program analyses, do. Undoubtedly, some dynamically safe programs will be excluded, e.g., most type systems will reject `if 2 + 2 == 4 then "hello" else 5` as an expression of type `String`. But, in exchange, accepted programs are free by construction of any misbehaviors the type system's type safety theorem rules out. The real question is: how do we design type systems that have useful type safety theorems...?
The language comes from Gödel's incompleteness theorems, in which there exist true statements that cannot be proven true, i.e. validated.
A given non-trivial computer program can be relied on to produce results consistent with its definition (its specification), but this cannot be proven in all cases.
It's not very complicated.
> This is precisely the rôle of the foundations of mathematics (or perhaps I should say a foundation, because there exist many competing ones): to provide a system whose consistency need not be questioned, and on top of which the rest of mathematics can be built.
This is what Russell and Whitehead had in mind when they wrote their magnum opus "Principia Mathematica" in the early 20th century. Gödel proved that their program was flawed. Surely you knew this?
> Also, it seems you misunderstand Gödel/Turing/etc.'s result.
The misunderstanding is not mine.
Provability is always relative to a formal system. The formal system you (should) use to prove a program correct (with respect to its specification) isn't the program itself.
> Gödel proved that their program was flawed. Surely you knew this?
Gödel didn't prove the futility of a foundations for mathematics. Far from it. What Gödel proved futile is the search for a positive answer to Hilbert's Entscheidunsproblem: There is no decision procedure that, given an arbitrary proposition (in some sensible formal system capable of expressing all of mathematics), returns `true` if it is a theorem (i.e., it has proof) or `false` if it is not.
If you want to lecture someone else on mathematical logic, I'd advise you to actually learn it yourself. I'm far from an expert in the topic, but at least this much I know.
Your words, not mine, but Gödel did prove that a non-trivial logical system cannot be both complete and consistent. As Gödel phrased it, "Any consistent axiomatic system of mathematics will contain theorems which cannot be proven. If all the theorems of an axiomatic system can be proven then the system is inconsistent, and thus has theorems which can be proven both true and false."
Gödel's result don't address futility, but completeness. That's why his theorems have the name they do.
> The formal system you (should) use to prove a program correct (with respect to its specification) isn't the program itself.
This refers to the classic case of using a larger system to prove the consistency of a smaller one, but it suffers from the problem that the larger system inherits all the problems it resolves in the smaller one.
> If you want to lecture someone ...
This is either beneath you, or it should be.
I'm sorry, but 'catnaroek is completely justified here. Multiple people have told you that you are simply factually wrong in your interpretation of the halting problem, and you are acting arrogant about it. If you tone back the arrogance a bit ("Surely you knew this?", "The misunderstanding is not mine") and concede that, potentially, it's not the case that everyone else is wrong and you're right, you might understand what your error is.
It's a very common mistake and is frequently mis-taught, especially by teachers who are unfamiliar with fields of research that actually care about the implications of the halting problem and of Gödel's theorems (both in computer science and in mathematics) and just know it as a curiosity. So I've been very patient about this. But as I pointed out to you in another comment, you are misreading what these things say in a way that should be very obvious once you state in formal terms what it is that you're claiming, and it would be worth you trying to acknowledge this.
Source: https://en.wikipedia.org/wiki/Halting_problem
Quote: "Alan Turing proved in 1936 that a general algorithm to solve the halting problem for all possible program-input pairs cannot exist." (emphasis added)
> Multiple people have told you that you are simply factually wrong ...
So as the number of people who object increases, the chances that I am wrong also increases? This is an argumentum ad populum, a logical error, and it is not how science works. Imagine being a scientist, someone for whom authority means nothing, and evidence means everything.
In your next post, rise to the occasion and post evidence (as I have done) instead of opinion, or don't post.
You don't need to solve the Halting problem (or find a way around Rice's theorem, etc.) to write a single correct program and prove it so. A-whole-nother story is if you want a decision procedure for whether an arbitrary program in a Turing-complete language satisfies an arbitrary specification. Such a decision procedure would be nice to have, alas, provably cannot possibly exist.
To give an analogy, consider these two apparently contradictory facts:
(0) Real number [assuming a representation that supports the usual arithmetic operations] equality is only semidecidable: There is a procedure that, given two arbitrary reals, loops forever if they are equal, but halts if they aren't. You can't do better than this.
(1) You can easily tell that the real numbers 1+3 and 2+2 are equal. [You can, right?]
The “contradiction” is resolved by noting that the given reals 1+3 and 2+2 aren't arbitrary, but were chosen to be equal right from the beginning, obviating the need to use the aforementioned procedure.
The way around the Halting problem is very similar: Don't write arbitrary programs. Rather, design your programs right from the beginning so that you can prove whatever you need to prove about them. Typically, this is only possible if the program and the proof are developed together, rather than the latter after the former.
This much math you need to know if you want to lecture others on the Internet. :-p
> but were chosen to be equal right from the beginning
While this was almost certainly the case, it's sufficient for them to have been chosen so as to be decidably comparable.
Indeed. :-)
The system you outline works perfectly as long as you limit yourself to provable assertions. But Gödel's theorems have led to examples of unprovable assertions, thus moving beyond the hypothetical into a realm that might collide with future algorithms, likely to be much more complex than typical modern algorithms, including some that may mistakenly be believed to be proven correct.
If we're balancing a bank's accounts, I think we're safe. In the future, when we start modeling the human brain's activities in code, this topic will likely seem less trivial, and the task of avoiding "arbitrary programs," and undecidable assertions (or even recognizing them in all cases), won't seem so easy.
> This much math you need to know if you want to lecture others on the Internet.
My original objection was completely appropriate to its context.
Of course. And if a formal system doesn't let you prove the theorems you want, you would just switch formal systems.
> But Gödel's theorems have led to examples of unprovable assertions, thus moving beyond the hypothetical into a realm that might collide with future algorithms likely to be much more complex than typical modern algorithms, including some that may mistakenly be believed to be proven correct.
Programming is applied logic, not religion. And a proof doesn't need to be “believed”, it just has to abide by the rules of a formal system. In some formal systems, like intensional type theory, verifying this is a matter of performing a syntactic check.
> If we're balancing a bank's accounts, I think we're safe.
I wouldn't be so sure.
> In the future, when we start modeling the human brain's activities in code, this topic will likely seem less trivial,
I see this as more of a problem for specification writers than programmers. Since I don't find myself writing specifications so often, this is basically Not My Problem (tm). Even if I wrote specifications for a living, I'm not dishonest or delusional enough to charge clients for doing something I actually can't do, like specifying a program that claims to be an accurate model of the human brain.
> and the task of avoiding "arbitrary programs," and undecidable assertions (or even recognizing them in all cases), won't seem so easy.
I don't see what's so hard about sticking to program structures (e.g., structural recursion) for which convenient proof principles exist (e.g., structural induction).
Please, get yourself a little bit of mathematical education before posting your next reply. You're so stubbornly wrong it's painful to see.
You seem to be contradicting your original claim, that it is impossible to prove any non-trivial program correct. Is this because you believe the program to balance a bank's accounts is trivial? Do you also believe that a C compiler is trivial?
I guess we never defined what you meant by "non-trivial." If your position is that the vast majority of software in the world today is "trivial," sure, I'd agree with you. But that's not really a meaning of "trivial" that anyone expected.
You seem to be mixing up where the "for all" lies. The result is:
There does not exist a procedure that, for all (program, input) pairs, the procedure will say whether the program halts for that input.
{p | Ɐ(f,i): p(f,i) says whether f(i) will halt } = ∅
For all (program, input) pairs, there does not exist a procedure that will say whether the program halts for that input.
Ɐ(f,i): {p | p(f,i) says whether f(i) will halt } = ∅
What is at issue is your incorrect assertions about what your evidence says. We read it, it contradicts you, everyone points this out, and you just ignore it and get louder.
Not at all. My original objection was to the claim that a program could be proven correct, without any qualifiers. Any program, not all programs. As stated, it's a false claim.
Your detailed comparison doesn't apply to my objection, which is to an unqualified claim.
> everyone points this out ...
Again, this is a logical error. Science is not a popularity contest, and in this specific context, straw polls resolve nothing.
> you just ignore it and get louder.
I wonder if you know how to have a discussion like this, in which there are only ideas, no personalities, and no place for ad hominem arguments?
Let's be precise.
Let P be the set of all programs.
Let C(s) ⊂ P be the set of programs correct relative to specification s.
{p ∈ C(s) | p, s ⊢ p ∈ C(s)} is large enough to be useful
> As stated, it's a false claim.
You have said this repeatedly, but all you have done in support of it is point at the Halting problem. The Halting problem says:
∃p ∈ P s.t. ¬(p ⊢ p ∈ C(halts)) ∧ ¬(p ⊢ p ∉ C(halts))
> [T]he Turing Halting problem (https://en.wikipedia.org/wiki/Halting_problem) demonstrates that one cannot establish that a non-trivial program is "provably correct."
I see no way to read that but as a claim that:
(∃p ∈ P s.t. ¬(p ⊢ p ∈ C(halts)) ∧ ¬(p ⊢ p ∉ C(halts))) → ((p,s ⊢ p ∈ C(s)) → p is trivial)
Note that it's quite true that
(∃p ∈ P s.t. ¬(p ⊢ p ∈ C(halts)) ∧ ¬(p ⊢ p ∉ C(halts))) → ((p,s ⊢ p ∈ C(s)) → *s* is trivial)
> Again, this is a logical error. Science is not a popularity contest, and in this specific context, straw polls resolve nothing.
I am not deciding it by poll. I am pointing out that there are objections to your reasoning that you have not addressed and persist in not addressing - despite them being made abundantly clear, repeatedly.
> I wonder if you know how to have a discussion like this, in which there are only ideas, no personalities, and no place for ad hominem arguments?
You're accusing me, as a person, of not understanding that a discussion like this has no place for accusations against a person? My complaint was not about you as a person, but about the form of your arguments in this discussion.
I have already done so. Did you read my comment about existential vs. universal quantifiers? Can you respond to it?
This was the original claim:
> It's false -- the Turing Halting problem (https://en.wikipedia.org/wiki/Halting_problem) demonstrates that one cannot establish that a non-trivial program is "provably correct."
This is the statement you quoted from Wikipedia:
> Quote: "Alan Turing proved in 1936 that a general algorithm to solve the halting problem for all possible program-input pairs cannot exist."
Do you agree or disagree that the quantifiers in these two statements are different? Do you agree or disagree that "the Turing Halting problem demonstrates that one cannot establish that every single non-trivial program is either 'provably correct' or 'provably incorrect'" is a different claim than the one originally made?
http://research.microsoft.com/apps/mobile/news.aspx?post=/en...
Also, Knuth in TAoCP spends significant time proving his programs correct.
Further, there is a compiler that is asserted to be proven correct: http://compcert.inria.fr/
Now it is possible you are working with a different definition of "proved correct" than I am thinking.
... and then someone finds a bug in the specification which is provably correctly implemented.
Using gets() to read the input can be provably correct. All you have to do is remove any requirements for security from the program's specification, and specify that the program will always be used in circumstances when the expected input datum will be less than a certain length.
... and then the hardware is buggy or failing. That RAM bit flips and you're screwed. The machine as a whole isn't provably correct.
Detecting overflows and throwing nice exceptions instead of continuing execution with garbage values isn't the same thing as ensuring correctness.
Java does array bounds checking in principle, but it is usually optimized out of the machine code. Isn't it then virtually just as susceptible to hardware error as C? And the JVM is written in C anyway.
https://www.cs.princeton.edu/~appel/papers/memerr.pdf [2003]
Which one?
https://en.wikipedia.org/wiki/List_of_Java_virtual_machines
Depending which one we are speaking about, they are implemented in Assembly, C, C++ or even Java.
As a programmer, if the specification is wrong, it's Not My Fault (tm). If you want me to write specifications, well, pay me to do it! I guarantee dramatically better results than the usual crap.
> The machine as a whole isn't provably correct.
As a programmer, defects in the machine are Not My Problem (tm). In any case, hardware vendors have a much better track record than software developers at delivering products that meet strict quality standards.
We're no longer discussing correctness, but assignment of blame.
As an aside, I want to clarify that I'm not advocating being a bad team player. The point to assigning blame isn't demonizing the developer of the faulty component, or reducing cooperation between developers of different components to the bare minimum. The point is just reducing the cost of fixing the problem.
If one program misuses another, usually the fix can be an alteration in either one or both. The used program can be expanded to accept the "misuse" which is actually legitimate but not in the requirements. Or the using program can be altered not to generate the misuse.
Sometimes what is fixed is chosen for non-technical reasons, like: the best place to fix it it is in such and such code, but ... it's too widely used to touch / not controlled by our group and we need a fix now / closed source and not getting fixed by the vendor {until next year|EVER} / ...
When in doubt, ask the specification. If there was no specification, why was any code written at all?
> If one program misuses another, usually the fix can be an alteration in either one or both.
Actually, there are three possibilities:
(0) The used program doesn't comply with its specification.
(1) The using program doesn't comply with its specification.
(2) The specifications of both programs are mutually inconsistent. In which case, it's a programming mistake to connect both programs.
> The used program can be expanded to accept the "misuse" which is actually legitimate but not in the requirements.
If it isn't in the specification, it isn't legitimate, period.
> Or the using program can be altered not to generate the misuse.
Sure.
You have some goal you're trying to achieve, or why was a specification written at all? If you find that the existing specification is not the optimal path to that goal, you may very well want to change the specification. In which case, it's entirely legitimate.
So the requirements/specification/program complex exists Just Because. Humans decided they want that: for their amusement, for the sake of supporting some enterprise or solving a problem, or to try to sell to other humans.
The complex contains several different representations because that's what it takes to bridge the gap between stating the requirements and making the machine carry them out.
A proof is something internal to that complex: that the specification corresponds to the requirements, and that the program implements the specification.
If we had just one artifact: a specification that executes, then there would be no concept of proof any more.
There is only the question whether the specification that was expressed is the one that was intended in the mind. That equivalence is no more susceptible to proof than, say, the correspondence between the Ceasar salad that the waiter just put on your table (and which you clearly specified) and the idea of whether you actually wanted one, or did you mistakenly say "Ceasar salad" in spite of having wanted a soup.
Plus, there is the external question of whether a specification has unintended consequences. That basically amounts to "you say you want that, but maybe you should revise what you want because of these bad things".
"You say you want plaintext passwords to be stored for easier recovery, and that can certainly be implemented (provably correctly, too) but consider the following ramifications ..."
It is possible for an executable functional specification to have unbearably bad performance for production use. In that case, the programmer has to reimplement the program in a more efficient (but perhaps less obvious) way and supply a proof that the reimplementation is functionally equivalent to the original executable specification.
Proofs aren't going away anytime soon.
> There is only the question whether the specification that was expressed is the one that was intended in the mind.
If other people can't bother communicating what they really want, that is absolutely Not My Problem (tm).
> Plus, there is the external question of whether a specification has unintended consequences.
If other people can't analyze the logical consequences of what they wish for, that is absolutely Not My Problem (tm). The most I can do is point at contradictions in the requirements.
I used to work in a facility where they'd test systems for radiation hardness. Get the system running, then shoot a proton beam travelling a significant fraction of the speed of light directly at the processor. It doesn't matter if the code was proven correct Dijkstra, it will eventually manifest bugs under these conditions.
[1] practically we resort to empirical testing to confirm that hardware conforms to its spec. But as your sibling says, that's no excuse not to do better in the places where we can.
Of course this is a disadvantage if you don't have sufficient experience in the problem domain. Sometimes I resort to writing prototypes in a script language in that case, translating the best design to the low-level language.
While that certainly can't be a bad thing, you just have to keep in mind that it forces you to think about a specific set of details – the ones that matter for the machine ("how many bytes will the binary representation of this username require") – and it may fool you into forgetting to think about higher-level concerns ("Does å compare equally to å?").
Avoiding unnecessary abstractions is important but at the same time those abstractions were invented for a reason. Basically the Go vs generics debate, except even more rudimentary. It's fine if your code doesn't need those abstractions, it sucks badly if it does (eg. gobject)
Just look at any C collection library for things like maps compared to C++.
Algol, PL/I, Mesa, Cedar, Modula-2 and many other languages of similar age or older than C, do offer both higher and lower level mechanisms.
The tradeoff is that the task at hand tends to have more implementation details in it than in higher level languages, but as you said, this isn't always bad.
The same code would be much simpler with C++ templates, but the "C being simple" really translates into limited, then you have that some have who never learned how to use macros and this unfounded and misunderstood fear of goto that gives you a nice long lines of error checking, each that that are duplicated if statements character by character where a goto and a single error handler would have worked.
Perhaps this is an exception, but low-level in my case did not correspond to simple code.
Although developers skipping return value checks is true in most languages.
#1 The submitted article is very good. #2 I'd add to it, avoid pointer arithmetic when possible. Use array notation instead. Typically the difference in execution speed is zero to nil. #3 I'd really like a pragma that forces an exception for unchecked return values. Something like
int DoSomeThing(/* whatever*/) #pragma exit "unchecked non_zero"
Yes, which is why I disagree with Go's approach for error codes as return values. I'm not saying that exceptions are the right solution everywhere, but if you return a error code, you should make it pretty hard to ignore it. In languages with Algebraic Data Types it's very easy to use Maybe or a Error(code) | Success(result) type. You've then got to explicitly deconstruct that type to get the result, so it's a bit harder to just forget handling the error.
> The first rule of C is don't write C if you can avoid it.