Alexis King (tweet):

The type systems provided by mainstream languages have grown vastly more sophisticated, but how much value does that complexity actually provide programmers in practice? I would like to make the case that it is somewhat less than one might think. While at times convenient, invariants can be captured in the type system using a small set of simple tools applied in principled fashion, and while fancy type systems may be convenient, they have misled many programmers by obscuring what is possible to model without built-in type system support. This talk aims to provide a simple shift in perspective, plus a set of concrete design principles, to make modeling invariants in types feel accessible to the working programmer without fancy language support.

“Type system as obligation tracker” is a catchy phrase, like her previous “parse, don’t validate” (Hacker News).

See also: Matt Diephouse.

Nicolas Seriot (Hacker News, Reddit):

The core Unicode algorithms (normalization, casing, bidi, collation) are deliberately bounded, but UTS #35 transliteration rules, under their natural unbounded semantics, are not. This is a result I haven’t found published before.

These rules ship as locale data in ICU, the Unicode library shipped in operating systems, browsers, runtimes, and databases. Whether a given rule file terminates on a given input is undecidable.

[…]

To prove UTS #35 universality, we compile 2-tag systems (Post, 1943), a model proven universal (Cocke & Minsky, 1964), into transliteration rules.

[…]

Transliteration rules were designed to turn “é” into “e”. Three lines of them can compute the Collatz function.

KT_Music:

Inspired by this, I tried creating an implementation that “solves #Sudoku” using only UTS#35 transformation rules 😎

Previously:

• Outlandish SQLite Recursive Query Examples
• Solving the “Miracle Sudoku” in Prolog
• Sudoku Solver

Nicolas Seriot (Hacker News):

Engineering folklore holds that Jira (Atlassian’s project-tracking tool) is Turing-complete. Existing claims point vaguely at automation features without exhibiting a reduction. This article supplies a proof, with setup instructions and execution trace.

[…]

Minsky proved this model Turing-complete (1967). Exhibiting it in Jira’s automation language therefore establishes the reduction. Here is how the model maps onto Jira:

Minsky Machine	Jira
Register A	Count of linked issues of type Bug
Register B	Count of linked issues of type Task
Program Counter	Status of a single Epic issue
Dispatch Table	Jira Automation rules, one per instruction state
Clock	Automation-triggered transitions, or external re-triggering past chain caps