Viewing profile — balddenimhero

Similar to the experiences of other commenters, I find the LaTeX edit-compile-review cycle to only grow unreasonably slow when none of the incremental compilation features are used…

SAT/SMT solving is indeed a much more structured approach and I agree that the analogy does not work too well for the backtracking part. I think that it rather applies to the well-…

Datalog-ish query languages sure is a fun area to be working in. Such DSLs exist for various domains and, like Semmle's codeQL or the more academic Soufflé, Glean focuses on the do…

Here, "inverse" is an abbreviation of "multiplicative inverse" (aka. the reciprocal). Granted, shortening it to just "inverse" is misleading, but the name has stuck.

It is fun to read the source of old games for gems like the discussed `Q_rsqrt` function. However, one often wonders what the limits/assumptions/guarantees of such tricks are so I'…

What a coincidence. I've also been looking into crossword generation recently. Have a look ( https://bohlender.pro/blog/generating-crosswords-with-sat-sm... ) if you're interested …

While "soundness" and "completeness" are well-defined properties of deductive systems, using such formal methods for analysis of real-world systems requires their formalisation. Ho…

I didn't read it as a critique of formal program analysis either. In fact, several aspects of his approach can be found in formal verification of probabilistic systems. However to …

Application of formal methods is always an interesting read, and this article is a gentle introduction to some of the ideas exploited in probabilistic model checking. However to me…