Equational

Not so long ago a good friend of mine mentioned his need for 'formal properties' in his code.   I asked him if he had already made the code purely monadic. He had. "Good", I said, "because the 'cheap route to formal properties' is first to ‘monadize' your code, and then 'reverse it' by bringing in 'co-execution'".  That last part needs some development.  Formal properties are not only about execution, actually mostly not about execution, but more about formal properties of state. So while you do need to show execution invariants, you often much more need to show that the ‘results’ happen within stateful invariants (e.g. of the ledger). The easiest way to do this is to  deconstruct / co-execute the state model backwards. This 'backwards' logic must 'match-up' with the 'forward execution' (monadic) model. My view has always been comonads are easiest for this, especially if your stateful model (e.g. a blockcha...

Dog Drives Car  Silly me shared the following picture with my sister-in-law yesterday, as she was stuck in a massive traffic jam with her dog (in photo) in her mini.  "How did you make the picture" was the question. "PowerPoint" was my reply. I used PowerPoint for that photo because it took me three minutes, and I had a slide deck open. Stop, you might say, this has nothing to do with programming, or software designs! It does if we want to design a software where a dog drives. Yet how would we approach that? Here I tell you how I have designed and communicated designs of 'big and bold' softwares quickly and with good properties. And will also sketch out how to approach exotic requirements, such as dogs driving cars. Arrows Away! Let me show you how I work. This how I use to draw design 28 years ago (from my PhD thesis): This is how I would have drawn that design 18 years ago (~2004): Here I use arrows to represent flows. Arrows are used to capture the Lagran...