This post is a summary of links related to coding and software I followed and read (sometimes, skimmed over) in the past week. Its purpose is both to serve as a high-level personal log and as a potential source of interesting (or not so interesting) links. Entries are provided in no particular order with minimal comments…
2017-04-17 Monday
: A formally proved adventure game: There is no dead end in the game, every states has a path that leads to a winning state.
: The model checker that is used by tttm. What's interesting is that it works directly on C/C++ source files. Could probably be adapted to work on Java files, if this is not already done...
Is there library support for FOL or propositional logic? - Google Groups
: Some discussion on the idris-lang mailing about adding native First-Order Logic support in the language
2017-04-18 Tuesday
Enquête sur les modes d’existence
: (in French) Criticism of Latour's book and more generally Latour's philosophy. Interesting counterpoint while I am trying to use Latour's concepts to better understand software and our relationship with it.
: (in French) Another criticism, this time of Object-Oriented Ontology and Speculative Realism
: Is it possible, and useful, to write CSS in TDD mode, with automated tests? Not sure this post provides a positive answer...
2017-04-19 Wednesday
Types + Properties = Software: designing with types
: Relinking to a classical series of post on Type-Driven Development in F#.
: Short description of Lean Development as a complement to Lean Manufacturing, by one of the foremost French expert on Lean
: How to use org-mode in Spacemacs. As I do a lot of pairing in Spacemacs those days, I need to beef up my skills with this environment and retarget my muscles memory to new keystrokes sequences...
abailly/yak-o-matic: visualize your yaks
: Thinking of reviving this old project, written with Willem van den Ende at Agile Open France 2013, whose purpose was visualising a dependency graph of tasks given an org-mode file.
2017-04-20 Thursday
: Some fascinating note on the use of category theory as an abstract assembly language to generate equations that are fed to Z3 theorem prover.
encryption - How do I compute the approximate entropy of a bit string? - Stack Overflow
: I have been working at the end of the week on a small coding challenge: Write a script that emulates the behavior of cat /dev/random, e.g. that generates an infinite stream of as-random-an-possible bytes. My first thought was : How do I test the randomness of a stream of bytes, and this started some research on the web on how to compute entropy of a string
: I chose to use this stream cipher algorithm to generate my stream of random bytes, encryting a stream of bytes coming from a network card put in promiscuous mode. It is reasonably straightforward to understand and implement and generates good "randomness"
: An article from Ron Rivest describing Spritz, an alternative to RC4.
2017-04-21 Friday
Entropy and Random Number Generators @ Calomel.org
: Helpful post on how to compute "entropy" for random generators. Link to the Ent tool
Haskell for all: Use Haskell for shell scripting
: I of course chose to write my random generation script in Haskell, trying to use as few dependencies as possible: I managed to get it working using only what's provided by GHC 8.0.2 distribution. Here is an alternative and more expressive way of writing scripts in Haskell.
2017-04-22 Saturday
: Reference implementation of Salsa algorithm in plain old C. salsafamily-20071225.pdf provides more details and rationale on this family of algorithms. This lead me to more stuff on PRNGs and how to gather entropy from the system:
: Something definitely fun I would love to work on!
2017-04-23 Sunday
A haskell implementation of a pseudo-random number generator using Salsa20 algorithm
: Final implementation of my pseudo-random bytes generator in Haskell
: I started to use compression ratio as a proxy for entropy of a finite stream of bytes but replaced it with direct measurement of Shannon's entropy, using the standard formula to compute the number of bits needed to represent all elements of a finite stream X with probability of occurence for each letter of p_i.
ARM Releases Machine Readable Architecture Specification – Alastair Reid – Researcher at ARM Ltd
: Another fascinating post on the use of formal specifications, this time in the realm of hardware architecture.
Forget about project planning; it just doesn't work | Alex Katsanos | Pulse | LinkedIn
: Looks like waterfall does not very well in "traditional" engineering either...
Testing Theories of American Politics
: Can we empirically demonstrate how policies are formed and driven? This article shows the answer is yes by testing actual decisions against theories of whose interest these decisions serve. Would definitely be interested in a similar study for Europe...