5 ms·
SQLite with a Fine-Toothed Comb (2016)
- siscia 8y agoCompletely unrelated, but maybe I can use the deep knowledge of HN. Browsing from the article I ended up in the page of tis-interpreter that says "You can also use TrustInSoft to maintain compliance or reach certification according to the norms EN-50128/IEEE 1558." [1] How does this compliance process work? Some of you have experience? [1]: https://trust-in-soft.com/industries/rail/ https://trust-in-soft.com/industries/rail/
- pascal_cuoq 8y agoYou should contact them[1]. TrustInSoft has a document that matches the classes of defects that its analyzer can guarantee the absence of to the vocabulary and recommendations of EN 50128. If you are preoccupied by this standard in particular, I'm sure that this document would make things clearer. N.B.: You had drifted away from the description of tis-interpreter at some point before you arrived to https://trust-in-soft.com/industries/rail/ https://trust-in-soft.com/industries/rail/ . While nothing prevents you from finding tis-interpreter useful in application of EN 50128, the page was written with TrustInSoft Analyzer in mind. TrustInSoft Analyzer is a static analyzer that propagates through the program sets of values (“abstract values” is the technical term[2]) instead of the concrete values corresponding to specific inputs that tis-interpreter propagates. As a result, TIS Analyzer can guarantee the absence of unwanted behaviors for all possible inputs. This is what makes it valuable from the point of view of software safety. [1] disclosure: by “them”, I mean “us”, since I'm a co-founder and work there [2] see https://en.wikipedia.org/wiki/Abstract_interpretation https://en.wikipedia.org/wiki/Abstract_interpretation
- collinf 8y agoRichard Hipp (creator of SQLite) had this to say about Rust and SQLite in the comments: > Rewriting SQLite in Rust, or some other trendy “safe” language, would not help. In fact it might hurt. Prof. Regehr did not find problems with SQLite. He found constructs in the SQLite source code which under a strict reading of the C standards have “undefined behaviour”, which means that the compiler can generate whatever machine code it wants without it being called a compiler bug. That’s an important finding. But as it happens, no modern compilers that we know of actually interpret any of the SQLite source code in an unexpected or harmful way. We know this, because we have tested the SQLite machine code – every single instruction – using many different compilers, on many different CPU architectures and operating systems and with many different compile-time options. So there is nothing wrong with the sqlite3.so or sqlite3.dylib or winsqlite3.dll library that is happily running on your computer. Those files contain no source code, and hence no UB. The point of Prof. Regehr’s post (as I understand it) is the the C programming language as evolved to contain such byzantine rules that even experts find it difficult to write complex programs that do not contain UB. The rules of rust are less byzantine (so far – give it time :-)) and so in theory it should be easier to write programs in rust that do not contain UB. That’s all well and good. But it does not relieve the programmer of the responsibility of testing the machine code to make sure it really does work as intended. The rust compiler contains bugs. (I don’t know what they are but I feel sure there must be some.) Some well-formed rust programs will generate machine code that behaves differently from what the programmer expected. In the case of rust we get to call these “compiler bugs” whereas in the C-language world such occurrences are more often labeled “undefined behavior”. But whatever you call it, the outcome is the same: the program does not work. And the only way to find these problems is to thoroughly test the actual machine code. And that is where rust falls down. Because it is a newer language, it does not have (afaik) tools like gcov that are so helpful for doing machine-code testing. Nor are there multiple independently-developed rust compilers for diversity testing. Perhaps that situation will change as rust becomes more popular, but that is the situation for now.
- pcwalton 8y agoOne problem with this argument is that SQLite is primarily used as a source-level embeddable library. That is, most users of SQLite don't use the official binaries and instead build the source code themselves. So, in practice, the source code, not the official blessed binary, is what matters. When upgrading compilers, developers of apps that embed SQLite don't typically check to ensure that upstream SQLite has tested the new version of their compiler. They just upgrade their compiler and assume that the new version will continue to compile their SQLite source properly. If the new version of the compiler happens to compile programs with undefined behavior differently, then problems can arise.
- SloopJon 8y agoRight, and the much vaunted test suite is proprietary, so the typical end user can't reproduce this test of "every single instruction." Not that I'm taking sides here. I'm really interested in both the extensive testing that the SQLite team does, and the analysis that John blogs about.
- pjmlp 8y agoCompiler bugs are supposed to get fixed. In C regarding UB, everything goes every single time the compiler gets upgraded.
- dangerbird2 8y agoIn many cases, what is considered UB in the C standard is a widely accepted and documented extension in the vast majority of compilers. For example, nonstrict aliases are UB in ISO C, but are defined language extensions in MSVC, GCC, clang, and many other compiler vendors.
- pjmlp 8y agoNow try to maintain a large C codebase stable and safe across such variety of compilers.
- 8y ago
- lixtra 8y agoAnother call for boringcc[0]. [0] https://news.ycombinator.com/item?id=10772841 https://news.ycombinator.com/item?id=10772841
- jokoon 8y agoI wonder if there are enough statically compiled languages out there. Not to be arrogant, but it doesn't seem new and/or recent languages are picking up fast enough, because their syntax is just not simple enough. I see many languages, and I never really find one that is interesting to me. I recently found volt, and I thought this language was really awesome. Then I realized that it is garbage collected. D is fine, but it has too many high level constructs (OOP and al) which I don't find useful. Rust is okay, but to me syntax matters most, and to me rust is too far from C. All of this shows that you cannot beat C. I just want a language that picks up from C, has the ease of use and readability of python, doesn't include high-level constructs as first class citizen, and compiles to LLVM or machine code. I wish I had the skills to build such language. C++ is close, but its slow compilation and its backward compatibility with C are not good.
- faceplanted 8y agoSounds like you want Rust with Python's syntax
- adwn 8y ago> All of this shows that you cannot beat C. No, all of this shows that you have very peculiar preferences and demands, some of which are more emotional than technical. > I just want a language that picks up from C, has the ease of use and readability of python These two requirements are mutually exclusive.
- cryptonector 8y agoNim does that. But I myself don't want Python-style syntax. I like braces and dislike semantic indentation -- part of it is that I like showmatch, and part of my aesthetic sense.
- chris_mc 8y agoNim? nim-lang.org It's GC, but that can be turned off and you can use manual memory management or you can simply use one of a handful of GC methods that work for you (in my experience, the GC is very performant). It has easy syntax like Python. It can be compiled to C, C++, ObjC, or JS (currently). It has tons of meta-programming features like templates, macros, etc. It can be cross-compiled fairly easily to almost any platform. It has whatever high level stuff you want to use, or just don't use them. It's not 1.0 yet, but it's pretty stable overall and the current release is feature-full enough that you could do just about anything with it that you want, right now. It's also got a really easy to use FFI. It's also about as fast as C, in practice.