We're not done building the boring stuff or solving the hard problems either. One is, well, boring and the other is...hard. Easy enough to proxy out prompts to OpenAI for your next funding round, though.
Other languages that make heavy usage of non-ASCII Unicode characters (such as Lean) often have tooling support such that one can type '\' along with some combination of ASCII characters to generate characters like '≈', '≠' and 'ƒ'. Along with searchable documentation for the whole mapping of shorthand codes to the mapped Unicode values, of course.
Code is read more than written, so I have grown to appreciate programming languages that lean into non-ASCII characters for semantic clarity :)
In event sourced systems, you project the event stream into read models, of which there can be many (relational, time series, etc.) If you're familiar with functional programming, it is essentially a fold operation over the stream of events into a single state.
Having worked with event sourced systems in the past, there are benefits in having a persisted explicit event history, but there is much added complexity (how do those read models actually get generated? how do you version the model? do you have snapshots of your read models?). In my experience, the additional complexity was not worth it for most contexts in which the pattern was applied...
I would recommend two. F# in Action [1] by Isaac Abraham is a great (and recent) introduction to the F# language. For a more philosophical, domain-oriented book, you can't go wrong with Scott Wlaschin's Domain Modeling Made Functional book[2]. Scott's blog[3] is also must-read material.
I had discovered Scott’s blog in the last couple of days while searching for resources related to writing lexers and parsers in F#. It is indeed a great resource!
Thank you for your other recommendations, I’ve just ordered both books!
It may be sacrilege to say this, but I have adopted Retool in my organization for the purposes of quick-and-dirty internal apps that are essentially thin GUIs around internal data stores. It has worked out well for us and even stodgy backend engineers like myself can be productive with it.
Congratulations on the publication! As a dabbler in strictly typed functional programming languages like Scala and F#, I have always been curious about proof-oriented languages such as Coq or Agda, but found it difficult to justify the time investment. Lean seems to position itself as a theorem proving language that also supports general-purpose programs. Looking forward to digging into your book!
Those other languages are also definitely worth learning. Happily, there's lots of cross-transfer of ideas and skills between them, so learning one will make the others easier. I got my start in dependent types with Software Foundations and Coq, and that was very helpful when learning Agda and Idris later. Similarly, skills from them transferred quite readily to Lean.
Lean4 is intended to be both, while Idris is more on the programming side and Agda - one the proof side. Maybe I'm mistaken about Idris, but Agda really doesn't prioritize programming: library handling, ffi, and tooling are all rudimentary.
Get with the times. We have tasked one AI with generating the prompts for the second AI. The two machines now sit in the corner generating and grading papers at each other over a USB cord. The kids love it. The parents are a little upset that their kids no longer have to attend the classroom, but such complaints disappear when they see how much everyone's grades have improved. SATs come in a few months and, given the class GPA, we are confident everyone will do well.
Yeah, I've known about Gleam, but I don't recall exactly why I wasn't too compelled to use it. I installed it with brew a while back, I tried a few basic examples and since then it's just been sitting there. I guess I should revisit. But thanks for the reminder anyway.
My understanding is that the 'linear' terminology derives from the field of Linear Logic[1]. But, I am by no means an expert on theoretical computer science etymology!
