I’ve been told the best way to learn is to do so let’s do some propositional logic with Coq. I got these exercises from the first two sessions of “The Incredible Proof Machine“.
I’m not sure how to translate contexts in sequent calculus other than making everything above the bar an input and everything below the bar an output so some of the exercises did not have analogs (like flipping the order of the premises). I either skipped those or made a best effort translation.
I’ve been in this game for a bit now and have observed a few patterns. What follows is a list of patterns about software infrastructure and how it can be managed or mismanaged depending on your perspective. The list is in no particular order or ranking. Continue reading
Most implementations of generators end up being state machines. This means instead of implementing explicit state machines one can use generators to keep the state implicit and let the compiler do the hard work of converting the generator to an explicit state machine. The downside of generator based approach is that it becomes much harder to serialize the state for persistence. The upside is there is less juggling of state overall because one can use the control flow facilities of the language in which the generator is embedded to keep track of the state. Continue reading
It’s time to bury this argument. It is no longer valid. (Actually it was never valid and I’ve just accepted this now).
We now have gradually typed languages that allow for mixing and matching the best aspects of both paradigms. I’ve also recently started to appreciate the value of a good type system. The compiler flagging weird data flow is very valuable and helpful in exploring the problem domain. I now think if given the choice it’s always better to use a statically typed language unless the shape of the data is determined at runtime. If the application is highly dynamic then there isn’t much to be gained from using a statically typed language and the iteration speed of a dynamically typed language is probably more valuable than compiler/type enforced correctness. Then again this trade-off is moot with languages like TypeScript so time to have the cake and eat it too.
State machines are everywhere but I don’t think they get enough air time. To remedy the situation I’m going to present an implementation in TypeScript and use it to model a very simple elevator. Continue reading
TypeScript continues to be amazing. Anders and team are doing an incredible job making the language accessible and at the same time powerful enough to express interesting invariants that can be encoded with conditional and mapping types.
I’m currently working on a workflow toolkit and building it in TypeScript has allowed me to express the message dispatch logic in a type safe way. Putting the pieces together has been a lot of fun so I’m going to outline the pattern in case others find it useful. Continue reading
Slightly enhanced version of the code is now on NPM and GitHub.
So it turns out that TypeScript doesn’t really have incremental compilation. This means if I rely on some 3rd party modules then recompiling anything that depends on that 3rd party module will transitively recompile everything. I understand that TypeScript is not a build system so delegating those responsibilities to one is a sensible design decision. The trouble with build systems is they can get pretty hairy pretty fast and ideally I want to avoid the overhead of one. Fortunately we can avoid the hairy parts of a build system by using a few symlinks and declaration files. Continue reading
I’ve been playing around with a few multi-paradigm programming languages. The most recent one is called Picat. It’s a hybrid language that is a mix of logic, imperative, actor, and functional paradigms with built-in constraint solvers and planners. That’s a lot to take in so whenever I’m faced with a language with roots in the logic paradigm the first thing I try to do is solve “SEND + MORE = MONEY” cryptarithmetic puzzle. It’s a small and manageable problem and there are at least two ways to solve it so it allows one to exercise several features of the logic and constraint paradigms. Continue reading
tl;dr Badly designed DSLs create unnecessary complexity and lead to more problems than they actually solve.
One of my frustrations with the DevOps and cloud infrastructure tools is that most of them are badly designed DSLs that eschew all features of modern programming languages. Continue reading