I often sketch out ideas on paper before I start really coding them up. The benefit is that I can take advantage of two dimensions, cross things out, draw lines, and so on.
I’d like to start perhaps getting a bit more formal in my sketches before I bring them to real code.
Does anyone else do this with some level of formality? If so, what notations do you use?
Popular contenders are APL (it started as this sort of thing anyway, but is ill-suited to object-oriented problem solving which is often required given the ultimate target languages), the Z Notation and its derivatives, UML…
(Note that I’m not necessarily asking for something that’s sound, formally specified, executable, or anything like that…though if they are that’s fine. The only requirement is that they’re usable with only pen and paper.)
To visually see the data flow through the algorithm/system, I sometimes like to draw flowcharts or diagrams that sometimes remotely resemble some kind of UML diagram.
To formally reason about the system/algorithm I’m working on, I use declarative modelling languages like TLA+ and Alloy to model important/complex parts of the system at a high level of abstraction. These languages are often rooted in first-order logic plus some other useful theory (e.g. set theory or relational algebra), allowing you to write abstract models of your system and its structure using mathematical objects like sets, functions, relations, etc, which you can easily reason about without having to get bogged down in implementation details (e.g. what data structure should I use here) at the design stage. The main benefit of using these modelling languages is that they often come with tool support for model checking or model finding, which exhaustively check the entire state space of the model for different kinds of safety, liveness, and deadlock freedom properties you specify, in finite scopes. These so called “lightweight formal methods” are super useful for catching design errors early on, rather than hoping to catch them later during implementation with hand-written unit tests etc (not to say that testing, especially property-based testing with QuichCheck-like tools isn’t useful).
Predicate logic. Love me some predicate logic.
Unsurprisingly I use TLA+, which was originally intended to be handwritten. Lamport didn’t think it was possible to model check at first!
How does it help when written on paper and not auto-checked by software? Honestly curious!
As Lamport says, “Writing is nature’s way of telling us how lousy our thinking is”. If I say “at least one node is always online”, do I mean
∃n ∈ Nodes: □Online(n)or□∃ n ∈ Nodes: Online(n)? One says “One of the nodes in the system is alive for the entire lifetime of the system” and the other ways “at all points in the system, there is at least one node (not necessarily the same one) that is online.” Very different meanings! I can get away with ambiguity in the English, but if writing it as predicate logic I have to pick one.Assuming to be like a proof. My experience with TLA was that simply by enumerating the cases the software was trying to catch, you could start to see the problems in your assumptions.
Nothing. I hate handwriting and only do this when I need to draw (flows or other stuff where 2d is important)
But every time I stub out something or do pseudocode (rarely), it’s in a plain text file.
Shameless plug: I have an in-development, not-entirely-successful answer to this question: https://hexdocs.pm/pantagruel/readme.html#content
Rarely the challenges for me are algorithms or mathematical, however frequently I’m faced with modeling a domain. Event storming is a useful technique for managing a domain complexity in the kind of rigor that a programmer could appreciate.
When exploring ideas, I write out long-form sentences and paragraphs. If my mind is racing and my hands can’t keep up, I’ll resort to a ‘stream of consciousness’ type of writing; a string of words making no grammatical sense. I find both of these techniques helpful because if I get interrupted, I can reread what I’ve written and usually have an easy time continuing where I left off.
If I’m trying to write code on paper, I try to do something that resembles Wirth’s Program Development by Stepwise Refinement. I write in the language I intend to code with, usually with a bit of shorthand borrowed from mathematics (LaTeX’s \in and \exists come to mind). Writing things out with pen and paper loosely following the methodology in the above paper helps me better spot when I’m making design decisions that should be made explicit.
Ultimately, the key reason I enjoy programming with pen and paper is because I love to write with fountain pens :)
While I used to love doing UML and Z-Notations early in my career and in the university and I still go with UML for my personal work or for when I have to provide formal/concrete design documents for anything. But I have never seen them formally used or enforced at any of the places at work - probably because startups where you have to iterate fast. Pen and papers or whiteboards with rough sketches are mostly the way to go.
Any time it requires more than a little text, it’s going into a text editor for me. My penmanship is awful, and I can key in text significantly faster than I can write it legibly by hand. I have a folder full of markdown for these kinds of notes.
I do still frequently do diagrams on paper or white boards. For those, I generally use a flowchart, with symbols adapted from these to suit the task at hand. If the diagram goes with the markdown I mentioned above, I use the VSCode ‘paste image’ extension to make a snapshot of the chart land with the textual notes. I actually like that extension so much that it has caused me to keep VSCode around primarily for markdown editing. (And also for PlatformIO recently).