1.

Note, the site breaks the back button.

1.

Straight up immoral is what it is

1. 7
Notes
• what is md5_id?

The id of md5, of course

(More seriously, this is a good companion to https://jacobian.org/2021/apr/7/embrace-the-grind/)

1. 11

This post only shows that specifications written in temporal logic don’t compose well. Fair enough.

However, this is far from the only kind of specifications that could be used for formal methods. In particular, it looks like nowadays some concurrent separation logic is the way to go; in particular, Iris https://iris-project.org/, a project which, among other achievements, presents several papers on POPL each year. The main advancement made by Iris—using commutative monoids to represent resources [which are great for representing specs due to being the best things to compose!] and invariants to represent immutable state—seems like something that could be applied to the example in the post with great success, producing a composable specification (assuming, possibly, the presence of a shared clock that drives the blinkers EDIT: looking at the post more closely, it seems that it is okay if the blinkers blink at unpredictable rates? If so, there is no need for a shared clock at all and everything simplifies a lot).

The way this could be done is by modelling a blinker in two parts: first, the opaque blob that says “this is a blinker with such and such properties”, and second, a unique, non-shareable resource one instance of each exists for each instance of a blinker; this non-shareable resource is parameterized by the state in which the blinker currently is. This “state” is not necessarily the state of the variables that the blinker uses, it can be any data structure at all (for example, when modelling some concurrent linearizable queue or something, the state could be just the list of the elements, regardless of the inner workings). Then, the opaque blobs, which contain the heavy logic behind the blinkers, never need to be expected in-depth, and to compose several blinkers, one just has to describe the relations between their user-visible states.

If you want to know more, be sure to check the website!

Disclaimer: I’d spent at least half a year doing formal proofs of a complex concurrent data structure in Iris, though I’m not affiliated with the Iris project.

1. 2

I’m reading some paper now, but my outside view base prior is caution. Not because there’s anything I see in the logic, but just because Iris came out in 2014 and there don’t yet seem to be a lot of examples of composing independent “real-world” Iris specs. The blinker is just an instructive example to showcase frame problems. Even if a specification language makes it specifically easy, it could run into problems composing larger dependent specifications.

1. 4

I have some perspective on why Iris hasn’t been widely used.

• The paper on Iris was published in 2015. However, this is only the logic itself, with no tooling to accompany it. The paper introducing the Coq library for working with Iris (“Iris Proof Mode”) was published in 2017. It is unlikely that anyone aside from professional logicians would sit down to draw some circles, squares, and triangles (the symbols Iris uses for various modalities) with pen and paper in the meantime.
• If I recall correctly (and I haven’t had an extensive hands-on experience with TLA+, so could be mistaken), then TLA+ allows writing arbitrary specifications, but nothing is there to check if they are sensible and relate to code in any way. This makes the task of writing specs easy, but at the expense of being completely sure that the code fits the spec. The scope of Iris is much broader, however. You could just write some specs, compose them and hope that the code fulfills them, but this is not how Iris is marketed. Instead, it is positioned to be used to prove the correctness of mind-bogging concurrent data structures. And let me tell you, this is hard! Each non-trivial line of code—that is, some line that affects the global state of the system—takes anywhere from two hours to several days to prove. The half a year that I was working with Iris, I was proving a single lock-free data structure. While it consisted of multiple interacting components, it is still some long time. I could have just written the specs for each component and be done with it—actually, this is what I did in the first week or so—and just ensure manually that the specs make sense, but then Iris would not be helping much, the challenge in our case was not with the specs, but with the interleavings of lock-free code.
• Iris itself is great, I never had a problem with it. However, the buggy and obscure mess that is Coq was the bane of my existence. Besides having to learn Coq—which, let’s just say, few people do—and having to learn the Iris framework, one must also be prepared to learn what to do when Coq refuses to find a type class instance or unify X with X, or loses the ability to automatically reason about arithmetic in the middle of the proof, so one has to prove things like a + (b + c) = (a + b) + c manually. This is a huge barrier for entry, so it’s not a surprise that few people use Coq with some framework as complex as Iris. Unfortunately, I don’t know of any other language that is more production-ready than Coq and yet still is able to host Iris.

To answer your doubts about Iris scaling well—in my experience, the specs do turn out exactly as intrusive or opaque as they need to be to convey what the component does. I was proving real, production code, and I was able to split my proof across the exact same boundaries that the original code has, providing a separate specification for each class, without any changes to the code to accommodate proofs whatsoever, and then composing those specifications in order to prove the correctness of the encompassing classes.

So, I think that adoption of Iris is a technological problem and not some fundamental issue with composition of specifications.

1.

Just wanted to echo this:

“…TLA+ allows writing arbitrary specifications, but nothing is there to check if they are sensible and relate to code in any way…”

I looked for something like this (for at least Java, C++, JavaScript code bases), but could not find any. I think this is a significant impediment to wider adoption of TLA+.

1.

I really need to write about why it is this way and some of the stuff the community is doing to change that. tl;dr refinement is a hard problem

(I agree it’s an adoption barrier, but it’s not the most “efficient” adoption barrier rn.)

1. 2

Have you considered how users might express LaTeX math notation in your markup language? Users who write math-heavy documents are often an afterthought when designing specs like this. There’s the traditional $...$ and $$...$$ for inline and block math, but if you want something less intrusive you might take Scholarly Markdown’s approach that fails gracefully in the absence of a math renderer.

1. 1

if you want something less intrusive you might take Scholarly Markdown’s approach that fails gracefully in the absence of a math renderer

This just seems to be backwards-compatibility with other Markdown renderers, which I’m not really striving for. Nor do I want to overload existing syntax, that would be quite messy.

Of course, falling back to just printing the raw expression could be done.

What syntax you consider for something less intrusive than  and $$? 1. 2 Some options: • I think the ... and $$... syntax is what people who write math will reach for out of habit. But if it poses parsing difficulties, you might choose to use ... for inline and choose another method for block math. • I’m not a fan of the LaTeX  syntax for block math, mostly because the \ character can be a burden to type on some non-English keyboard layouts. Nevertheless it’s an option. • You could go full LaTeX and look for $$...$$ and \begin{align}...\end{align} etc. • Instead of overloading existing code block syntax, you could always introduce a new type of block delimiter like this, to be consistent with your existing markup. This would also placate users who like the ...$$ syntax. :) $$
block math here
$ I do personally think that in the absence of special notation just for math, “named” code blocks are the way to go. That way each block can be sent to the appropriate postprocessor, and you have a simple avenue for extensibility later. (for example, chemists might ask you to support SMILES diagrams) You can also take a look at how Madoko and MathPix Markdown handle math. 1. 2 I do personally think that in the absence of special notation just for math, “named” code blocks are the way to go. That way each block can be sent to the appropriate postprocessor, and you have a simple avenue for extensibility later. (for example, chemists might ask you to support SMILES diagrams) That’s what rST does: there’s general inline (role) and block (directive) syntax, and the build process exposed an intermediate doctree representation. Opens up all sorts of useful extensions. 1. 1 I wrote a response to this: Grind Smarter, not Harder 1. 3 That being said, code is systematized rigour, it’s mathematics/logic that can be computer validated rather than supposed to shakey parsing of the human mind. So, ahm, just take a few weeks and learn some basic python? [earlier] I read papers, I don’t run experiments I can tell. 1. 1 I found this very enlightening as to some of the difficulties of composing different specifications. I’ve often leaned on specification approaches that model processes and communication. I would imagine if you defined the blinkers as a independent processes (ala PlusCal) the composition would be closer to a developers intuition. 1. 2 There’s a tricky subtlety here. PlusCal is a DSL that compiles to TLA+. If you look at the compiled TLA+, you’ll see that the different processes are represented by a global pc state that tracks the label of both. There’s no point where we have two specifications, we have just one specification with two subcomponents. The equivalent “composition” here would be putting two processes in separate files, compiling both to TLA+, and then writing a third spec that instantiates both files and composes A!Spec and B!Spec. 1. 1 That makes perfect sense. I guess I’m trying to say PlusCal is designed to represent process and communication between them, and that composes well without the same difficulties described. It seems that is because they avoid the problems described of specification composing. The DSL could be used to compose a larger spec via careful concatenation. There isn’t really tooling to support it so not really any solution to the problem. But I find it interesting that re-framing the concept to an existing DSL may provide route to composition that matches a larger set of developers mental model. 1. 3 The issue with the two blinker example looks more like a limitation of this particular specification language (TLA+?), than a fundamental issue with formal specifications in general? While implementation hiding doesn’t necessarily work (or even make sense) with formal methods, I see no reason that the two blinker example couldn’t “compose” using linear logic as the specification language. Of course there’s new math needed in the two blinker case, e.g. update reordering. More is, after all, different. But I’m pretty sure that new math should be generalizable to larger numbers of blinkers. 1. 1 The issue with the two blinker example looks more like a limitation of this particular specification language (TLA+?) LTL! TLA+ adds a lot of extra machinery to make composing and refining specs easier that I didn’t want to get into in this demo. I see no reason that the two blinker example couldn’t “compose” using linear logic as the specification language. Please share an example! But I’m pretty sure that new math should be generalizable to larger numbers of blinkers. That’s a limitation of explaining this: I chose blinkers because it’s a very simple spec that showcases well the examples of the frame problem and dependent specs. Most specifications aren’t nearly this simple, not anywhere close. Math that handles a blinker spec might be overfitting and completely break down when you instead have multiple readers and writers with a shared queue. 1. 4 Just sent this to a friend of mine who wants to do 3D printing but hates most existing CAD tools, and now he’s really excited again. Thank you for sharing! 1. 1 Working on a talk about esolangs! And submitting The Crossover Project as a talk to a conf I really like 1. 1 Not loading for me. 1. 1 Strange, works fine for me :-$

1. 12

For a few years now, my response to this question is a counter-question:

Is reading/writing/arithmetic a science or an art?

Of course they’re neither. So it is with programming. You can use programming to do either science or art. But it’s just a tool.

There’s a cool question in the middle of the post. As I understand “ontological status”:

Where does the essence of a program reside?

Following Peter Naur, the unsatisfactory answer for most programs is, “in the programmers’ heads,” with the increasing implication of incoherence for large teams of programmers. Very large programs stop being comprehensible in humanistic terms, and start to rather resemble egregores. Like gods, or bureaucracies.

But I think we can do better, retain more control. A better answer, for well-written programs, is “in the space of inputs accepted, as categorized into different regimes with relatively linear processing logic.” Personally I like to visualize this input space as tests. Haskell/OCaml and APL propose alternative approaches that also seem plausible.

1. 3

But I think we can do better, retain more control. A better answer, for well-written programs, is “in the space of inputs accepted, as categorized into different regimes with relatively linear processing logic.” Personally I like to visualize this input space as tests. Haskell/OCaml and APL propose alternative approaches that also seem plausible.

I think I’d say you were somewhere near the mark with “egregore”, a cool word I just learned from your comment, but that the space of what a program “really is” extends not just to the minds of the people who write / maintain / administer it, but to the entire substrate it operates on, including physical hardware and the minds of its users and the shadowy, informal conceptual footprint it has therein. Much like the way that, say, a fictional / mythological / historical narrative exists in the often vast and highly ramified space between authors and readers and cultural context.

Not that there’s anything wrong with trying to delineate space-of-inputs-accepted and the like - just that we’re probably kidding ourselves if we think that we’re going to get to comprehensibility at all, for large things. Creating bounded spaces within which to reason and exercising extreme humility about the big pictures seems like as good as it’s ever really going to get, most days.

1. 2

Very valid considerations. My answer to that is: if making it large gives up control over it, perhaps we shouldn’t make it large.

As a concrete example, one project I work on explores maintaining control over a full computing stack with the following limitations:

• single instruction set (32-bit x86)
• single video mode (1024x768 with 256 colors)
• single fixed-width font (8x16px)
• mostly text mode
• only ATA (IDE) disk drives, running in a slow non-DMA mode

It’ll add features over time, but only so fast as I can figure out how to track – and communicate to others! – the input space. For example, it doesn’t have a mouse yet, because I don’t understand it and because I don’t want to just pull in a mouse driver without understanding it and having thorough unit tests (in machine code!) for it.

Basically I want to consider the possibility that humanity has been adopting computers way too aggressively and introducing lots of risks to all of society at large. I don’t want software to go from explosive adoption to another hamstrung and stiflingly regulated field, bureaucracy by other means. There’s too much promise here for that, even if we take a hundred years to slowly develop it.

1. 2

Very valid considerations. My answer to that is: if making it large gives up control over it, perhaps we shouldn’t make it large. … Basically I want to consider the possibility that humanity has been adopting computers way too aggressively and introducing lots of risks to all of society at large.

Well said, even if I’m personally pretty sure the genie is out of the bottle at this point.

I don’t think I can really draw a clear line in my own mind between what bureaucracy is and what software is, but I welcome efforts to ameliorate and rate-limit the poisoning of things that seems to come with scaling software.

2. 0

Uh, writing is definitely an art?

1. 12

Not if I’m writing a grocery list.

1. 1

hmm. I was initially unsure reading this, but I think I agree writing a grocery list is probably not an art. I’m not shocked there’s an edge case here, but it’s interesting to think about. I guess the programming equivalent would be code ls or similar trivial cases

1. 5

It is by no means a rare edge case. If you assume all writing is art, that implies science is also art. Which is a reasonable and internally consistent interpretation of the terms, but not the frame of reference of the original question.

1. 2

Scientific writing (such as journal articles) is certainly an art. Many good scientists are bad at the writing.

1. 2

It’s a skill for sure, but that doesn’t necessarily make it an art. If I look at my own writing (which isn’t scientific but is technical) then the amount of creativity that’s involved isn’t much more than, say, fixing my bike: it requires a bit at times, but mostly it’s just working at it.

1. 2

It sounds like you aren’t bothered by the original question. Which is great; it’s not a very interesting question. I’m personally more curious what you think about the second half of my first comment :)

2. 6

It’s definitely a craft.

1. 3

That’s been my opinion for a long time now. Like other crafts it isn’t automatically included or excluded from other human activities - art, science, commerce, hobbies …

If you accept that then the question posed isn’t very interesting.

1.

I think the interesting question is whether it’s a craft or an engineering discipline.

2. 2

Not necessarily. Designing a building can an art, a science, or a combination of both. A friend of mine does ghost writing for non-fiction. Most of it follows a formula and neither of us would consider it art.

Words are a tool used to communicate the same way verbal speech is.

1. 1

But surely in ghostwriting non-fiction you still have choice in what words you use to convey the concepts?

1.

I’ve done a fair amount of technical writing for hire. Art enters the picture somewhere, to be sure, but where you’re writing to strict house standards and pre-set outlines it does have a way of driving most of the feeling of creative expression out of things. And I suppose that gets at how I understand “art” - a feeling as much as anything.

1. 22

It’s unclear if there’s any advantage to using this.

I like the idea of metadata, but there are already markdown extensions for that.

Unordered lists are enclosed with [] and ordered lists are enclosed with {}.

That’s the exact reverse of common notation, where {} is a set and [] is an array.

But nice effort.

1. 4

This is my reaction as well.

I think it’s great that @skuzzmiglet could scratch their own itch and build this, but to be honest I’ve been SO INCREDIBLY grateful for the widespread support of Markdown as a near universal markup supported in more and more contexts and applications that I look at every new variant and unfairly think “NOoooOOOOOooo! Here we go again!”.

1. 1

I like the idea of metadata, but there are already markdown extensions for that.

MultiMarkdown’s is only at the start of the document and does weird auto-detecting, frontmatter adds a dependency (YAML and TOML are overkill, JSON is verbose) and Pandoc’s metadata is limited to dates, titles and manpage data.

That’s the exact reverse of common notation, where {} is a set and [] is an array.

Aren’t sets and arrays both order-preserving?

1. 11

Arrays are order-preserving, sets are not. A set is an unordered collection of unique elements. Many programming languages order their sets, but that’s either purely an implementation detail or an intentional deviation from the math definition.

1. 2

an intentional deviation from the math definition

It’s not a deviation, but an extension; ordered sets are still valid as sets, so long as they have a membership predicate. Math sets are not ordered simply because they don’t need to be.

1. 3

Math sets are not ordered simply because they don’t need to be.

1. 2

Ha, good point. If we don’t accept the axiom of choice then there may be unordered sets which cannot be represented in terms of an ordered data structure. (That being said, I think the existence of an ordered data structure kind of assumes well-ordering is possible, but.)

2. 1

It’s not a deviation, but an extension; ordered sets are still valid as sets, so long as they have a membership predicate.

Nope! Ordering violates the first axiom of set theory:

https://en.m.wikipedia.org/wiki/Axiom_of_extensionality

1. 1

It does not. That is a definition of equality based on membership, and you can still define it that way on ordered sets. (It’s fine to have another, separate equivalence relation which takes order into account.)

1. 1

Oh there’s a subtle miscommunication going on here. You’re assuming that “ordered set” means what it would mean in math: a set with a pre-defined ordering of its elements?

I was assuming that “ordered set” meant what it (might) mean in a programming context: a “set that remembers original insertion order.” https://code.activestate.com/recipes/576694/

The first definition is compatible with the axiom of extensionality. But the second definition violates it because the set {A, B} would be quite different than the set {B, A}.

1. 1

I was operating under the programming definition of ‘ordered’.

My point is that you can construct an equivalence relation for ordered sets that treats {A, B} as equivalent to {B, A}, without sacrificing the ability to construct other equivalence relations that would distinguish the two.

2. 1

Sets are basically just predicates denoting membership. Bags add duplicates (which is what an unordered list is) and lists add a order on top of that.

1. 1

Order is not a well-defined operation on sets.

1. 2

Here’s a sample:

David Morgan-Mar created Chefthe following year(2002). While a cooking recipe might sound as arbitrary a system as other esolangs use, it differs in that recipes already are algorithms. […] Ian Bogost is just that masochist. He has been eating Chef recipes for fifteen years. Bogost has been teaching Chef to his creative coding students for that long, often leading to actual cooked dishes.

1. 2

I write technical documents in sphinx. What would you are the relative benefits of using Scrivener instead?

1. 4

Not OP, but I have used Scrivener for years, though for fiction. Here’s what I like about it, which may or may not actually be things you care about:

1. Long documents are broken up into smaller chunks (called scrivenings), with essentially arbitrary levels of nesting. You can select multiple of these and then have the main document area show all of those chunks together.
2. It has a powerful “compile” feature that can take your book and produce ready-to-go ebook and print formats (or Word, if you need to get the doc into someone else’s hands)
3. If you’re working on the kind of thing where you’d want to change the flow of the document, there’s a corkboard view that lets you move the individual scrivenings around
4. Store notes that are not part of the final doc in the same Scrivener doc, just in a separate folder within it. All neatly accessible in the UI.
5. Each scrivening can have its own metadata, tracking its status (first draft, second draft, final draft, etc.), or with notes specific to it.
6. Can sync with iOS for writing/updating on the go (I sometimes prefer to use my iPad for this)
7. Word count targets are nice when you’re trying to get a project done

I’m sure I’m leaving a lot of features out. This is one of those tools that I think will suit some people’s brains and not others. Kind of like todo list apps.

1. 1

I never used sphinx so I can’t comment on it, but @dangoor comment is spot on. I think that Scrivener is beneficial for those who are writing longer works as they can keep research, notes, links, and the content all in one place. It feels like a companion or an assistant, always ready to help you write your book.

1. 3

Did you write the typeup site in typeup? If so, could you share the source for the site?

1. 2

Sadly not, the current nesting rules don’t allow for multiline code in tables (I handwrote the HTML). I would love to bootstrap, though it may take some syntax bending. If you’re looking for more examples, https://git.sr.ht/~skuzzymiglet/typeup-doc/tree/master/item/example-document.tup has them.

New markup formats are sorta hard to actually use since so many webpages just take plain markdown. You could make scripts to open Vim and dump the converted text back but it’s a bit of a hassle for a rather small benefit (unless Lobsters, GitHub and MS Teams start supporting typeup :)). The hard solution would be Chrome/Firefox plugins and custom-extending everything.

1. 5

I don’t really see why I want his vs the dozens of existing wiki languages. It even sharea the thing I like least about markdown (using # for headers)

1. 3

Funnily enough using # for headers is the biggest thing I miss when writing rST instead of markdown.

1. 3

The annoying thing (to me) about MD header syntax is that the lower-level headers are much more visible than the higher level ones, which is backwards.

I’m not sure how to fix that, but it’s still annoying. (Textile’s “.h1” syntax just made no headers particularly visible, which wasn’t any better, really.)

1. 2

To me it’s that so many syntaxes use = for headings and # for ordered lists and Markdown breaks both of those at once with the weird header choice.

1. 1

Interesting. More # for lower-level headings is unintuitive to type, and increasing numbers of # reflect nesting better. I chose # for typeup because it’s the same for markdown, and as a character it can’t be improved much (I don’t mind borrowing from markdown)

1. 8

I like the metadata and table syntax, and I like the idea of a simpler-to-parse, indentation-insensitive Markdown alternative. But I don’t think I’d ever get used to [] for bulleted lists. The standard - format for lists is intuitive, and it’s the way I automatically type in text documents anyway, because most of my notes end up being deeply-nested bulleted lists.

Is it even possible to put multiple paragraphs under a single list item in typeup? From the looks of the spec, that can’t be done, which is a problem. Multiline list entries are a problem in most markup languages (Markdown implementations sometimes disagree on the level of indentation), so I was hoping that a less-finicky Markdown-like syntax would make this easier.

1. 6

Multiline list entries are a problem in most markup languages (Markdown implementations sometimes disagree on the level of indentation),

Have you heard the good word of CommonMark

(with apologies to @hwayne)

1. 3

Multiline list entries are a problem in most markup languages (Markdown implementations sometimes disagree on the level of indentation),

Have you heard the good word of reStructuredText

1. 1

Alternatively: GraphQL. Less dangerous than SQL, less tight coupling to the exact DB structure, but about as powerful.

Disclaimer: haven’t used it so far

1. 72

That’s a pretty major disclaimer!

1. 8

I’ve poked at GraphQL a couple times and repeatedly come to the conclusion that it makes a bunch of very domain specific trade-offs and can’t really be described as a query language at all.

Pretty much any form of accepting a subset of SQL is more general purpose, has better support for complex data models, can do graph adjacency or pivot tables and such which is where I’ve seen most ORMs even struggle.

I wish there were less clojure-flavored datalogs as query interfaces to be had.

1. 2

less clojure-flavored datalogs as query interfaces

Less?

1. 1

May I suggest Preql ?

(warning: shameless self-promotion)

2. 8

GraphQL is not a query language. It’s an RPC API abstraction.

1. 7

I’m not sure “not even having joins” is “about as powerful”.

1. 3

Indeed. I think the “QL” in GraphQL is misleading, unless you have a very basic definition of “query”.

1. 2

I’ve been using Hasura, and I can join to other tables (can’t do GROUP BY, though). I guess it depends on how you implement things?

(There may be some limits to Hasura’s joining that I’m not aware of - I’ve only tried to do very basic “follow the foreign-key and fetch some fields from that table” kind of things.)

2. 3

Except that one major difficulty of GraphQL is precisely to resolve GraphQL queries to SQL queries in an efficient way. Except if you use something like Hasura or similar which will do the work for you.

1. 1

We curently use postgraphile for reads and some basic write operations. Anything more complicated we make an API for it. Seems to work pretty well overall.