I had the pleasure of interviewing, befriending <a href=“https://lobste.rs/~zdsmith” rel=“ugc”>@zdsmith</a> whose passions are very close to my heart. He explores the different forms of notation (Iverson, Naur), makes <a href=“https://tacittalk.com/2024/09/27/Episode-5.html” rel=“ugc”>combinatory programming</a> approachable, ported <a href=“https://jnj.li/” rel=“ugc”>J to Janet</a>, created an ergonomic <a href=“https://pantagruel-language.com/” rel=“ugc”>notation</a> for requirements gathering, designed his own <a href=“https://blog.zdsmith.com/series/shorthands.html” rel=“ugc”>shorthands</a>, attended the Recurse center and much <a href=“https://buttondown.com/zdsmith/archive/” rel=“ugc”>more</a>. We talk about:

• tacit and combinatory programming
• array languages
• domain modeling and DSLs
• lisp vs. type systems
• management and motivation

<hr> Could you please introduce yourself? I’m a programmer from New York City. I have a variety of interests, primarily writing systems, systems of notation and poetics. Within the realm of programming, my closest focus is combinatory programming. I do my personal programming in Janet or <a href=“https://lfe.io/” rel=“ugc”>Lisp Flavored Erlang</a>. Traditional card games, still played in a given village for hundreds of years, are my true love in life (email me if you like them!) Card games are both complete systems and social mediums, happening between people. They don’t exist without people and help them interact. Games are <a href=“https://blog.zdsmith.com/posts/what-makes-a-good-culture-game.html” rel=“ugc”>culture</a>, evolving like food, language or dress. Modern games are designed, which I have less interest in. How did you discover combinatorics? To clarify, combinatorics is the study of sort of combinations of things while combinatory programming is using combinators, which I’m more interested in. One of the most salient features of array languages, especially J and APL is tacit programming (equivalent to point-free style in e.g. Haskell). Conor Hoekstra (<a href=“https://www.youtube.com/@code_report/videos” rel=“ugc”>codereport</a>) was the first person (I’m aware of) to say “hold on a second, there’s this whole realm of logic and mathematics called combinatoric logic. If we squint, these behaviors that we love so much in tacit programming are actually examples of combinators.” I found this concept very compelling. In particular, it prompted me to wonder whether we could pull that behavior out of the array world so that it was no longer tacit, what it would look like in generic programming languages. Conor even <a href=“https://tacittalk.com/2024/09/27/Episode-5.html” rel=“ugc”>interviewed you</a> about this! How have you employed combinatory programming at work or your other pursuits? What distinguishes me, I think, from many folks enjoying this, is that I’m interested in how to apply it to the actual work of programming, professionally or as an amateur, solo or in an organization. I’m a programmer, you’re a programmer, we write programs. I’m interested in this experience, the phenomenology of programming, how to make it easier, funner. Not only how to make it easier for myself to write programs, but to read other people’s programs too. That’s exactly the question I want to explore with combinators. Tacit programming is undoubtedly more terse; you type fewer characters. For an array language enthusiast, typing fewer characters is already the name of the game. But I want to extract it from that context, to explore whether they themselves make programs easier to read or write, instead of merely appreciating them for their theoretical beauty. They’re fun, exciting, tickle your brain. But compare it to functional programming, which has been relatively successful in industry, because you write fewer bugs with clearer intent using map instead of for loops, using destructuring and construction rather than in place mutation. I’ve had the benefit and privilege of working in places with this approach. So I’m interested how combinatory programming lives or dies in a real-world environment. But more recently I’ve been doing more management. I did refactor a small function at work with this style, in TypeScript. The code owner, understandably, said “please don’t do this”. It was not a point-free codebase. Ultimately, these techniques are political or social questions. If a long-lived codebases gradually became functional over time, it’s not because one engineer got really excited about Haskell and wrote functors and applicatives all over the place. There was actual a discussion that had to be made, with a social and political argument for why it was worth doing. I’m not at the point where I want to advocate to 100 engineers in my organization and say “alright, we should no longer use variables, no longer use named lambdas”. I want to experiment and see what the value of this stuff is in a real environment. How did you first discover programming, what were you doing before hearing Conor’s revelation? It was fairly late in life. In high school, I luckily had an APCS course in C and C++. I loved my teacher and the work, found it incredibly satisfying, but also very difficult manually constructing linked lists and managing memory. It was really hard to wrap my head around the connection between getting a program to compile and making programs that do useful work. So I didn’t follow up on programming at university. I didn’t graduate at all, I fixed laptops and did data recovery for 10 years, but realized that wasn’t what I wanted to do for the rest of my life and tried programming again. Python had become more popular, so I self-studied for 3 months in 2014. I had the enormous good fortune to find out about and get accepted into Hacker School (now <a href=“https://www.recurse.com/” rel=“ugc”>Recurse</a>). Many of the more intellectually rigorous and creative people writing software or about programming have gone there or are part of that community. And I got to spend 3 months with 55 of them in a single office for 4-5 days a week, just working on open source software, any project, but with collaboration, teaching, being taught. So I learned an extraordinary amount in a short time and got a job right after. I wrote in Python and Nim for a few years. I loved Erlang, BEAM, OTP etc. and ended up at an Elixir shop, but the last 5 years have been using TypeScript, professionally. What did you do with Nim in industry? My first programming job was at a logistics company with storage, vans and trucks. We had rudimentary software doing route planning in Python. But we had one incredibly hot loop with a (relatively) complex algorithm. I settled on Nim because it was fast with good c inter-op and a low barrier to entry. I was sufficiently green and naive that I underrated the price of introducing a new language no one else spoke into the tech stack. You have to be very fool-hardy to make that decision and I was in the right place at the right time. But it turned out perfectly fine! The code was simple and well-written enough that they just had to keep it running without any changes. At any rate, the company stopped existing before it became a problem. How do you view management? I also do half programming, half managing, but consider them quite similar, where software development’s like industrial engineering, with business analysts documenting or creating processes, tasks which can be performed by people, machines or programs according to cost, efficiency and accuracy. For me, hiring, training and caring for a person or provisioning an environment for a program, ensuring the computer has power, working parts etc. are similar. What’s your framework for all of this? I don’t see myself doing the same work when programming or managing. There are some tremendous, technically adept engineers who produce amazing things that others take and make useful. But most us aren’t like that. To be useful or “deliver value”, we must ensure we’re writing the right software for the right reasons while communicating to the right people what we’re doing and how to change it later. These are all important parts of making yourself and your code useful on the job. Guiding and advising engineers in such matters is management, to me. Good management won’t just think about being maximally useful for the organization but will help each engineer remain excited, have fun ad grow, if they want growth. Everything works better that way. I’ve worked with teams of brilliant engineers where we spent 6 months producing nothing of value because we weren’t going in the right direction and hadn’t determined whether the organization actually told us what they wanted or decided to buy this. That’s the ideal at least, arranging all of these necessary pieces to help engineers make useful things. How can we help our teammates grow, have fun, do these things? Implicit in your question is, you don’t have to be a manager to do this. Right! That’s so critical. Sometimes you’re the senior person in the team or lower on the totem pole, but you have e.g. the emotional intelligence to see when somebody’s stuck or gets more excited about something. The simplest advice is to ask yourself and your colleagues what motivates you individually. Programming’s fueled by flow states, excitement, curiosity. If you’re not feeling it, if you’re sluggish and uninspired, you can only do so much. This isn’t a mechanical field, but requires creativity and enthusiasm. An easy pitfall, especially for leaders, is assuming everybody’s motivated by the same stuff. Startup founders are often motivated by a vision of the future of software or the future of their product domain, but other people can be motivated by hard challenges, supporting and doing right by their team mates, or simply material compensation. For me, I’m committed to supporting my team and making sure they’re getting enough of what they need to stay motivated. What actually motivates you personally? As a manager, you want to help your team, but why do you want to work with a team? What about when you’re working on a personal project? In a professional scenario, anybody’s who’s been in a field for a long time comes to recognize that people are more important than what you’re actually doing at any moment. It’s certainly true that the software you write’s very likely to be thrown away within a year (and you should hope that it is!) The company you’re working in might not exist in 5 years (though you should hope it does). That’s the reality of the work. It’s rare that any particular software or program will make as much of an impact as the individuals you work with. You can form true relationships with them and impact each others’’ lives. We often miss how much we can impact other people’s lives by showing up in a certain way. Thinking about how I conduct my whole life, work included, I orient around how I can show up for the people I’ll crash into that day. For personal projects, a library or shorthand, I have almost diametrically opposed motivations. What does it mean for other people to engage with your work? What first hooked my to programming was opening a REPL, building, encoding a little system of rules with classes and methods, then watch it go. I love writing down what I know and producing novelty, actually seeing this complex system you can’t possibly keep in your head produce emergent behavior. For every project, I have an idea about some individual rules and primitives and want to discover what happens at that inflection moment when there’s enough there to move and change on their own steam. What scratched this itch before you (re)discovered programming? I’ve been making <a href=“https://en.wikipedia.org/wiki/Shorthand” rel=“ugc”>shorthands</a> and writing systems for myself since 2006. These are systems of rules and signs you elegantly compose to produce something useful. Writing music especially with other people also scratches that itch, with electronic or mechanical means. I used to compose generative or aleatoric music or translate a set of signs, information or data from some domain into the Western scale or another set of pitches! Piling a few relatively simple things which each fit into your head, on top of each other, gives you something complex and rich, indescribable! It’s like you have a little compression algorithm and are seeing what it decompresses to. There’s a long history of generative music in Lisp. <a href=“https://ccrma.stanford.edu/software/clm/” rel=“ugc”>Common Lisp Music</a>, <a href=“http://repmus.ircam.fr/openmusic/home” rel=“ugc”>Open Music</a>, <a href=“https://incudine.sourceforge.net/” rel=“ugc”>Incudine</a>, <a href=“https://www.opusmodus.com/” rel=“ugc”>OpusModus</a>, <a href=“https://github.com/ormf/cm” rel=“ugc”>Common Music</a>, <a href=“https://en.wikipedia.org/wiki/David_Cope” rel=“ugc”>David Cope</a>'s many books on GOFAI music. More recently I discovered <a href=“https://lisp.trane.studio/” rel=“ugc”>trane</a> written in Janet and from the array side, Marshall Lochbaum’s doing <a href=“https://mlochbaum.github.io/BQN-Musician/index.html” rel=“ugc”>music</a> with BQN, an array language and Stanley Jordan’s been <a href=“https://dl.acm.org/doi/pdf/10.1145/75144.75174” rel=“ugc”>using APL</a> for a long time. But you weren’t programming then, were you just throwing things at the wall or engaging with another body of work? More in the throwing things at the wall school. As an example, 20 years ago, I was thinking about how a musical score isn’t the same as a piece of music and is just a sketch, a blueprint. Thinking of <a href=“https://www.dynamicmath.xyz/strange-attractors/” rel=“ugc”>strange attractors</a>, where chaotic systems with enough points can define a trend, I thought layering many individual performances of a piece could approach the mean of the music itself. So I lined up as many performances of Schumann’s piano concerto in A Minor’s first movement, one of my favorite pieces, with normalized tempo and listened. Which array language did you learn first? I played around with J a bit and returned to the Recurse Center in 2021, where I <a href=“https://jnj.li/” rel=“ugc”>embedded</a> the J runtime into Janet. But I understand K the best, which ironically has middling support for tacit programming, but it tickles my brain and thinking in arrays is a really powerful mental tool. K has the least ranks which would require you to grok matrices and vectors. You can stick to low-dimensional arrays without being encouraged to pile on adverbs which change the rank of your verb. How much math did and do you know? Very little. Like many people, I was never really exposed to math and thought myself bad at it. Later, I read <a href=“https://worrydream.com/refs/Lockhart_2002_-_A_Mathematician’s_Lament.pdf” rel=“ugc”>A Mathematician’s Lament</a> and found it incredibly moving. I played around with number and group theory, programming simple things. The <a href=“https://oeis.org/” rel=“ugc”>On-Line Encyclopedia of Integer Sequences</a> is one of my favorite places ever. So I learned there’s a vast variety of structures and systems you can play with, but I only engage with them in a very shallow way. That’s why with combinatory stuff, it’s important for me to come back to practical programming. We can look at functional programming through category theory, which has produced useful programming techniques. But the techniques themselves have to be useful, critically, without understanding the theory. The whole point’s that we can put it on the computer and not have to suspend it in our heads anymore. People often learn lisp to overcome a hurdle. For me, it was macros. For array languages and K, I wanted to escape this rigid adherence to iterative for loops or reduce way of thinking. So it wasn’t terribly important to master linear algebra, because I don’t deal with those kinds of problems. Iverson and others wrote many books teaching math through APL and J. They’re really breezy, since you don’t have to do everything by hand. Most of calculus is learning rules of thumb, methods to solve or guess. But with a computational tool, it’s so easy! Iverson had a tremendous mind, Notation as a Tool of Thought is really wonderful. But you could make many counter arguments to the Iversonian array school’s idea of terseness unlocking clarity, faster thinking. Some say it overindexes on the wrong things. The time saved typing fewer characters is negiligible, because the real work in APL is rephrasing your problem unti it fits the model and your 10 symbols are correct, which can take as long as writing verbose Python. In a future with less code generated by humans, this matters even less. If AIs spit out and review hundreds of lines of Python, with no human in the loop, I’m not sure how array programming presents an alternative. <a href=“https://youtu.be/eVddGSTjEd0?si=pO1EHj8GQ6v-2Gbm&amp;t=51” rel=“ugc”>It’s the kids who are wrong.</a> I mean circling back, what does it mean for someone to engage with someone’s work? Why do we want to code in the first place? Restricting ourselves to personal projects or blog posts, my ideal was putting things out there with polish, dedicating myself to the project but also documenting it with a fun website, so I’m really creating something I can personally feel good about, a perfect realization of what I wanted to create. My ideal was that this was enough. But I became frustrated that I didn’t have people to talk about these things. You’ve mentioned shorthand a few times and this occupies a lot of my personal thinking. You’d be surprised to hear, but not a lot of people in my daily life are interested. Shocking, I know, but my friends, coworkers, loved ones think it’s cool but don’t want to create their own writing systems and discuss them! There’s a community <a href=“https://www.reddit.com/r/shorthand/” rel=“ugc”>on Reddit</a>, so I spend time there now. I also think a lot about poetics, the relationship between poetic form and mathematics, the use of mathematical techniques to <a href=“https://blog.zdsmith.com/posts/an-algebraic-sketch-of-poetic-form.html” rel=“ugc”>generate</a> poetic forms. I don’t have many people to discuss this with, so the reality’s that I don’t need people to use the software I write (though it’s incredibly gratifying when I hear people do) and I certainly don’t need people to tell me how smart I am, what a great blog post, but it’s really important for me to know who my audience is and engage in dialogue around the things which interest me. Perhaps I share to connect with others, create points of common and shared interests. For the full person, it’s important for me to know there’s someone on the other side who thinks any of this is as interesting as I do. I possess the feeling, if not conviction, that other programmers share many of my interests because they all feel so deeply connected. On the other hand, I’ve posted about card games and shorthand and watched them drop like stones. I have an SSG <a href=“https://bagatto.co/” rel=“ugc”>Bagatto</a> which people actually use, so people ask for help in different places. In their minds, they’re using a piece of software with a community, but to me it’s my weird little thing! The moment it hits the internet and is decontextualized, it just becomes part of the internet, of the literature. Recently, my partner got a kind, thoughtful email from a stranger and, it’s a truism, it is so nice to get a nice email. That’s a microcosm of everything. I want to be in a community and the community, my people, are just people who decided to put something out there. Call to Action: Send those emails! Tell obscure project how much you like their small projects and make friends! What cool people would you like to broadcast to the world? Conor Hoekstra is great, walking the line between theory and practice. He has all these nerdy interests but tries to popularize them in podcasts and on youtube. <a href=“https://jvns.ca/” rel=“ugc”>Julia Evans</a> does the same with fantastic zines. Anyone in New York should go to the Recurse Center’s events to meet people doing the same thing. I just went to Breakpoint which is like a science fair for people who get an idea, build a thing then take the extra step to make it accessible (via readme, making sure it compiles on other people’s machines or going to events). There’s also <a href=“https://toddwords.com/wordhack/” rel=“ugc”>wordhack</a>. How do you personally approach pretty websites and documentation? You can force it, honestly. There are ebbs and flows of motivation. You have to find a way to work with them, be okay with writing something down which you can return to in 6 months. There’s some sort of personal organization in making a system to find what you were half-way happy with before putting it away, which you can return to with fresh eyes and passion. <a href=“https://github.com/Voultapher/sort-research-rs/blob/main/writeup/unreasonable/text.md” rel=“ugc”>The unreasonable effectiveness of modern sorting algorithms</a> is relevant; industry and programming has continued to optimize because we’ve realized how magic numbers matter, per-computation, L1 caches and all of that. What makes a program beautiful? Because I think this goes right back to the question of form. The aesthetic experience of programming seems to me to be a direct engagement with a formal system, as instantiated in that part of our brain that has evolved to work with patterns. That’s why I think it’s aesthetically pleasing to write programs. And insofar as a program is an arrangement of concepts via relations into some form, it seems that we recognize that form as beautiful when it exhibits properties that we admire in other sets-of-relations, viz., mathematical objects, games, riddles, and so on. Symmetry, simplicity (as measured against productive power), an economy of unique objects, and so on. This is how I tend to think of it. But it’s a hypothesis I haven’t been able to test yet. It seems to me that if this is true, I should be able to communicate the beauty of a particular program, via translation, to someone who doesn’t know computer programming. I haven’t hit on an effective way to do that. To what extent should a program be a lookup table? Purely industrial programs will often be lookup tables. My personal programs are about systems, ideas I want to explore, so a readable, elegant expression of an “algorithm” is the most important thing. None of them need to sacrifice clarity and transparency for efficiency. Indeed, most of the stuff I write for work is just a big map and indexing into it. You can solve many problems this way. Make it a prefix tree if you really want to flex. Janet is a great exemplar of this, ruthlessly pragmatic. A lisp which throws away everything you’d expect of a traditional lisp if it leads to more convenient or pragmatic approaches. Famously like Clojure, Janet’s tuples and arrays aren’t linked lists, because repeated pointer dereferencing isn’t the most efficient way to write programs on modern hardware. But it has everything I want from a lisp: s-expressions and macros. How did you discover lisp and <a href=“https://janet-lang.org/docs/index.html” rel=“ugc”>Janet</a> specifically? Recurse is a wonderful place for finding out about the most esoteric and exotic things for programmers. In 2014, Haskell was most exemplary, with everyone wanting to learn Haskell and Hindley-Millner. Lisp is similar. As language family it’s fascinating, but as a social phenomenon too! It has an incredible reputation, earned and unearned. There’s that <a href=“https://xkcd.com/224/” rel=“ugc”>XKCD</a>, Let over Lambda, Paul Graham and Eric Raymond’s silly things. So early on, I was introduced to it as something incredibly powerful, hard to understand and very old. But I decided to really learn it from the inside out, 5 years ago, specifically to master macros, which I had only lightly encountered in industry but which seemed directly practical. So I decided to learn a lisp to explore and master macros, work through the books with etc. Janet was a Goldilocks thing for me. I wanted an every day language I could write command line utilities and script in. I would have learned Clojure, but the JVM means running a 45 line script would launch a huge VM which just wouldn’t cut it for me. Janet felt clean, didn’t have decades of cruft (though it does have cruft) and is fast and easy to use. **Short hands, <a href=“https://github.com/kparc/ksimple/blob/main/a.c” rel=“ugc”>Arthur-Whitney-style</a> C, tactic programming terseness and compression… They’re all pretty linked. ** I hypothesize the underlying value of tacit programming is reducing the conceptual inventory of a program, not the number of characters or tokens, but the size of the ontology. Less things exist in that universe when you remove a name in favor of a common pattern of function application. That’s what I want to compress. That’s my elevator pitch for combinator programming. If there’s any universal benefit to macros or Arthur Whitney’s style, it’s whether we can come up with names to encapsulate these common patterns or combinations of objects rather than just make our name shorter. In fact, I have no interest in shortening the names. I am highly skeptical of the school of thought claiming the more code you can <a href=“https://github.com/tlack/b-decoded?tab=readme-ov-file#arthur-style” rel=“ugc”>fit on your screen</a>, the better. But stripping unnecessary objects are really worth interrogating and investigating. I wouldn’t claim shorthand has similar aims. Shorthand is incredibly practical, it was a business tool for the whole era of writing until typewriters, for anyone who needed to write really fast then actually read what they wrote. For many people, it was an essential skill to make money, falling on the industrial not theoretical side. Yet what I want from my own shorthand system, what makes one beautiful or enjoyable (no longer pure utility but beauty and elegance), is reducing the number of things. I’ve written a bunch of software to design this over the last year. One of those programs takes the entire inventory finds all the unique concepts in the system and expresses the ratio between that and the inventory of sounds in the English language. There are, of course, more entities in my shorthand than sounds in English, but now you can think about economy. You can arbitrarily compress spoken English with more entities which are less utilized, but can you find the inflection point where you have the most bang for your buck getting the maximal compression without too complex of a system? Minimalism is why people find lisp so beautiful, especially scheme. They’ve tried to identify the smallest number of primitives necessary. If you look at <a href=“https://en.wikipedia.org/wiki/SKI_combinator_calculus” rel=“ugc”>SKI combinators</a>, we can express all Turing complete logic with three or really two primitives. We can also express everything with a Turing machine. But those aren’t good systems to actually use. I want to find the inflection point where a system is both easy and pleasing to use, but also sufficiently minimal for our aesthetic sense. To what extent do languages do this vs. frameworks for some domain? I think that’s the data model. I’m not a programming language creator. I have made languages for domain specific things but I’m not interested in creating a general purpose language. But representing a domain with enough primitives to say what you need without being verbose tickles my brain. Having few enough primitives which compose well that you can keep in your brain, is the name of the game for any business programming. Any time you need to model a domain, you need to create a language or a calculus, a few primitives or basic concepts which compose together to express everything that matters. That set me on fire about programming. I’ll be honest, I’m not super interested in logistics, but that basic challenge of modeling everything our logistic team knows and cares about, that’s fun! Type-driven programming is quite different from lisp. How does that influence your modeling? Working the last 5 years in TypeScript really colors this, as I’ve done very little work on larger codebases in lisp. I have done a lot of teamwork in Elixir and BEAM codebases, but I think type systems are a fantastic tool for data modeling in industry, where your code st be maximally understandable and modifiable to someone seeing it for the first time (including you in 6 months). Composing types is a really fantastic, especially with a fast compiler letting you do type inference and higher level typing which stays out of your way. I rely on the compiler a lot. On the other hand, when I’m writing something in e.g. Janet which is both dynamic and very mutable, I get very nervous and fearful about changing the data model. Immutability or types give you a lot of confidence. How do you jump into a new domain and truly understand it in order to then model it? This comes to my side project <a href=“https://pantagruel-language.com/” rel=“ugc”>Pantagruel</a>. Returning to the Iversonian question of <a href=“https://www.jsoftware.com/papers/tot.htm#” rel=“ugc”>Notation as a Tool of Thought</a>, what’s an appropriate notation for domains? A domain is entities, rules or invariants if you want to sound more mathy. Systems composed of things and rules or truths of how they interact. One of the real shames of our industry is that we know we have to truly understand a domain before doing anything on the computer, making sure you have the theory down. We know it’s critical and some of the thinkers I admire the most really hammer down on this. <a href=“https://gist.github.com/onlurking/fc5c81d18cfce9ff81bc968a7f342fb1” rel=“ugc”>Programming as Theory Building</a> is my bible. Rich Hickley talks about <a href=“https://www.youtube.com/watch?v=f84n5oFoZBc” rel=“ugc”>Hammock-driven development</a>. But we don’t have good notations or tools for this work. We just write it down with boxes and lines on a whiteboard or use natural languages, both crude and error-prone. My experimental language Pantagruel is a notation for describing systems. You can describe the rules of a card game, mathematical rules or tickets you need to implement. So we have a domain for our software like video clips which can combine into timelines, be organized in folders and you want to express some property of that system, like a folder can’t have a folder with 0 timelines in it. Pantagruel is a very simple notation designed for writing by hand to express these things tersely, but you can also write it on a computer and do static analysis to ensure you’ve not accidentally gone from a scalar to a vector, single to plural, which plain English wouldn’t catch. I want to see if it’s actually useful, better than the tools we have today. I came up with a set of syntactical constructions and expressed as many things as possible. If I found myself writing too much or thinking too hard about something, I would add a construct. But if I didn’t use something often or could simply combine others to get it, I could eliminate a construct. That’s how I generated Pantagruel. It looks nothing like it did when I first started it. My shorthand has gone through dozens of these iterations in the past year. Are there any other similar tools to Pantagruel? I’ve surprisingly not found any. The formal methods world is closest, but it has that theory vs. practice/industry issue. It’s very intensive to get a complete model of your domain up in them. The reward’s incredible power. But my little system’s explicitly easier to pick up (and less powerful). Unfortunately, anyone interested in formal systems or methods thinks my system is nonsense, not worth doing anything worth their time, while the rest of the world is scared off by propositional logic. Why do you think people don’t care? Some say “real engineers” should aim for perfectly correct code, but many don’t want to learn any “weird” tools. It’s a shame that many are surprisingly reluctant to engage with what looks like theory, logic or math. I think it stems from the way we teach mathematics and the unimportance we place on it as a society. I grew up thinking math wasn’t for me, after all. At the same time, most lines of code don’t have long lifetimes and formal methods aren’t suitable for a feature which might not last 6 months or when the consequence is a button in the wrong color.