This really has nothing to do on this list, but here I go... Languages are like gods : there can be only one, and its perfect, and everywhere, and we show our faith. Sure.. who wants to believe that crap ? Languages have flaws, they are (slightly) bugged to the core and we're so much into their usage^Wabuse that we dont see walls anymore. "Hey my windows works fine at home when installing every year !!"
You dismiss assisted code proof because proving code is not verified itself. What if it could be ? Actually it has been done with a compiler of a subset of C and a few ML like languages. Compiled assembly code of compiler was proven correct by humans. The ML like languages, along with type theory, are now used to study math theorems by writing them in types and proving the theorem by writing a program of that type. IIRC this is Curry-Howard correspondence. In languages like ocaml every expression has a static type, possibly removing all need for runtime type info. I also think the ocaml grammar and static typing sucks, but programs that compile *always* work and are fast. In 1996, a researcher named J.L Krivine took the theorem of the completeness of classical logic (we all use in science, math, programming), expressed it in type theory, and actually proved it by writing a step by step userland disassembler. Pure wtf, but true. Mind blower to me. Just like C, OCaml has skills in its semantics, but they both suck at grammar : parsing ml requires a full lex/yacc above and below gcc. Not really checked code but if the bug hasnt shown it must not exist. Or in the next release. Parsing lisp, i can explain to a 2 year old. Do it in *any* language. In less than 1kb. On the syntax, Lisp is the red pill. Languages like C let the humans do all the deducive work, though this is something machines do better. Are you reviewing the bits on your disk by hand after hard reboot ? No you write a program for that. Do you have to check every piece of assembled functionality in your OS by hand ? Yes because the code cannot understand the code. Checking for errors is good, machines are better than humans at repetitive tasks. I'm not saying it has to be automatized, just we could have had more powerful tools at hand if C was not an outdated tech the day it was made.. I'm not fixing this but we have to wake up. And fix the problems at their root. Not so OT actually ? That some system programmers still ignore much of the details of what was achieved in programming languages is no surprise, our community is broken by our beliefs that they are fighting on the same plane. To express all programs. Language esthetes fail to like C semantics, all lost in high-levelness or using C when too close to the metal. C programmers often not aware that non-fortran-like languages actually do wonders. Once again, I can only praise the C semantics for what is achieved by hand in this project. But i cannot shut up about its grammar. It is the worst wormed gift ever made to the programming world. Along with INTERCAL. Actually it was not really a gift, more of a prank. I'm not advising anyone let off C and those waiting for me to tell them some truth about programming languages are fucking zombies. But you cannot blind yourself into C like the world wants you to. There are way more beautiful things to see in this world, dont you know ? Grammar is the tool at the base of your trust : you assume you can express what your twisted and experienced mind wants to see in forming a sequence of tokens. In the grammar of C you assemble characters to form a tree of tokens. You cannot see them, just trust they are actually there. Or not : optimizations, defines, bad macros, missing ;, broken lexer, broken compiler,.. hairy errors. In symbolic computing to can actually avoid all duplication of code, review or even step-step through compilation, define new compilation macros, extending compiler e.g checking for some type of errors without duplicating code - true macros. - avoid needing so much complexity just for parsing/compiling => more trust, less to check by hand This is not because of the language itself, which is actually not better defined than C, but because of its parsability. Code is actually not text : it is a tree of tokens. I think I made my point, maybe now I'll try to shut up. And Christiano, you know, technically its only a rape if i do not consent. And `sed` threats dont really work on me. All in all, i trust all the distrust in OpenBSD to build an awesome product. I thought I'd share some distrust regarding some of our most important tools. Maybe not paranoia. Be safe =)
