ritter2a

Very interesting! Quite amusing that adding milk seems to be an unquestionable truth while adding sugar is considered destroying the flavour and adding pepper (which is not uncommon in India) appears to be unthinkable.

But I find it most surprising that the detailed rules say nothing about how long to steep the tea.

What about adding "echo sleep 0.01 >> ~/.bashrc" to their .bashrc (or whichever shell config file is used)?

At least for some form of mechanical clocks: There is an app for that :)

E.g., for Android, the "Watch Accuracy Meter", which can be found in the Play Store or the APK source of your choice, uses the phone's microphone to measure the frequency of mechanical watches.

I would say that the benefits you get from a habit of using SMT solvers depends a lot on the kind of problems you are working on.

If your problem is rather small and self-contained, you can really win a lot with these solvers. E.g. I used an ILP solver to fairly distribute tasks to a group of people based on a heuristic of familiarity between each person and the tasks. That's only a few constraints in the solver that saved me a lot of manual or suboptimal coding work. Similarly, it was easy enough to quickly check whether two graphs satisfy a custom condition that is close to (but not quite) isomorphism that I wanted to give a try.

If you are thinking of bigger, more complex tasks, the efficiency gains you get might vary more. If your problem produces many large solver queries, the chances are good that you will wait a long time for results. Without much practice, adjusting/augmenting your specification (and specifically in the case of ILP solvers: tuning the solver parameters) to reduce your solving times is a very non-trivial task. Either way, the solver probably won't bring you to 80% of the execution speed of a custom solution: I once sped up a task by 100-200x by replacing a Gurobi LP with a dumb, theoretically exponential, but easy to optimize custom implementation (the solver was however helpful for testing that the implementation was correct).

Lastly, in my experience, once a constraint system/model reaches a certain complexity, it is a lot more difficult to debug than code in a programming language. There are useful techniques and tricks for debugging solver models, but the tooling and the sequential execution of real code make debugging of traditional code less of a head ache.

Regarding interface stability: Indeed, the textual representation is not stable, things like added types in the representation of some instructions can happen when upgrading to a new version. However, to be entirely honest, in the last few years of updating LLVM-based research tools to newer LLVM versions, changes in the C++ API that required me to (sometimes just slightly) change my code happened a lot more often than changes in the textual representation...

I consider it a fun little game to guess for each mention of "Kafka" in a HN title, whether it means the author or the software. Definitely not trivial, since this time, I would have guessed "Kafka in Pieces" to be an introduction to the software, component by component.

Having written test cases for a similar semantic program analysis tool, I agree: Integer overflow is a very likely cause for such "obviously correct but actually wrong" program invariants. The C semantics can make this problem even worse since signed integer overflow is undefined, leaving the user of such a framework to the mercy of the design decisions of the creators of the framework regarding undefined behavior.

Well, there is the Hennessy&Patterson book, "Computer Architecture - A Quantitative Approach". The newer editions include modern features and follow industry's developments.

This will of course not be able to tell you all the black magic that is happening inside AMD's and Intel's newest designs. The software optimization manuals for these processors do include some more interesting insights, but especially the Intel ones are not the most entertaining read...

There will probably always be particular code transformations (algorithmic or target-machine-specific) that speed up your code and that your general purpose compilers will not find. (And that's good, because otherwise the compile time would be horrible!)

The good thing about compiler optimizations is not that they produce actual "optimal" binaries, but that they allow you to not care too much about performance when writing code (e.g. using abstractions that will be inlined, etc.) and still get a decent binary. If you then require more performance (which will probably not be the case for most applications) you can still search for bottlenecks and start optimizing by hand there.

You don't get quite this level of ambiguity with standard C, since it does not provide objects (in the object-oriented sense) with constructors, in contrast to C++ that is used in the Arduino environment (in C++, initialization order of global objects is indeed unspecified, inviting subtle bugs to occur).

However, many common C compilers provide methods to declare functions to run at initialization time, e.g. gcc's `constructor` attribute, opening this rabbit hole also for C programmers.