aarchi

Author here! I had a hunch that the typeclass resolution engine in the Coq typechecker could be Turing-complete, so I proved it by implementing a variant of Brainfuck in it. Feedback welcome.

PostgreSQL is Turing-complete, as proven by implementations of a cyclic tag system[0] and Turing machine[1]. The Mandelbrot set[2] and travelling-salesman problem[3] have also been implemented in it.

Transact-SQL is also Turing-complete, as proven by a Brainfuck implementation[4].

With that, you can theoretically compute anything :).

[0]: https://wiki.postgresql.org/wiki/Cyclic_Tag_System

[1]: https://blog.coelho.net/database/2013/08/17/turing-sql-1.htm...

[2]: https://wiki.postgresql.org/wiki/Mandelbrot_set

[3]: https://web.archive.org/web/20201111224603/http://assets.en....

[4]: https://stackoverflow.com/questions/900055/is-sql-or-even-ts...

I'm currently building a couple of regexp engines:

One, that's a formalization[0] in Coq with big-step semantics, which uncommonly has the intersection operator, and includes several equivalence relations and a proof of the pumping lemma, excepting one case (more on that below).

As a learning exercise and for historical reasons, I've also mostly ported Rust Cox's re1 engine to Rust[1], which includes VM matchers in the style of Henry Spencer, Ken Thompson, and Rob Pike. I also plan to port Doug McIlroy's engine[2], which is interesting for having intersection and complement and special handling for sublanguages, all the way down to just concatenation matched with Knuth-Morris-Pratt. I also want to examine the Rust (thanks burntsushi!), RE2, and Plan 9 engines in more depth.

Once I have time to get back to the project, I want to get back to my regular expression crossword puzzle solver. For that, I'm converting the hint regexps to DFAs, that match strings of some fixed length, and concatenating and intersecting them, until a single regexp is yielded, which should be a string literal, if the puzzle has a single solution. For backreferences, it's more tricky, but I plan on rewriting backreferences to the captured expression, where the lengths of both match, then either executing it with a stack like a pushdown automata or constructing a set of constraints on the characters by index.

As an aside: In my proof of the pumping lemma[3], I got stuck on the case for intersection and I'd love insight. Regular languages are closed under intersection, so the pumping lemma should hold for my implementation. I need to prove that if s =~ re1 and s =~ re2 can be pumped, then so can s =~ And re1 re2. s is is split into different substrings for re1 and re2, s = s11 ++ s12 ++ s13 = s21 ++ s22 ++ s23, then repeated an arbitrary number of times, (forall n, s11 ++ repeat s12 n ++ s13 =~ re1) and (forall n, s21 ++ repeat s22 n ++ s23 =~ re2). My intuition is that s11 = s21, s12 = s22, and s13 = s23, because they both match for the intersection, but I'm not convinced of that and haven't been able to formulate a proof for that.

0: https://github.com/thaliaarchi/recross-coq

1: https://github.com/thaliaarchi/re1-rust

2: https://github.com/arnoldrobbins/mcilroy-regex

3: https://github.com/thaliaarchi/recross-coq/blob/main/theorie...

The (preprint) paper links to its repository, where its code eventually will be. I suspect it will be pushed around August 2023, before USENIX Security'23, where it will be published.

https://github.com/sslab-gatech/autofz

> Other contamination was also found in or on: three buses, 42 houses, fourteen cars, five pigs, and 50,000 rolls of toilet paper

Why such a large figure for toilet paper? Is it somehow more easily contaminated by radiation?

This makes me want to dump all my TI-Basic programs from my calculator and put them into source control.

I just got a terrible idea: combine this with another project, that built Tetris in Conway's Game of Life. That would enable executing an arbitrary program in Tetris, simulated in Game of Life.

https://codegolf.stackexchange.com/questions/11880/build-a-w...

Zettelkästen certainly aren't new, as the technique was popularized in the 1950s and had been around for much longer.

Try doing it in Whitespace then :)

https://github.com/andrewarchi/ws-challenges

I've created a similar repo of puzzles, including Advent of Code, but solved in the Whitespace programming language. Even otherwise easy puzzles are made significantly more difficult in Whitespace, as it is a quite low-level language. The control flow feels like coding in assembly and the stack paradigm feels like a Forth. The challenge is fun, though, and I'm filling in the gaps of my (unofficial) standard library as I go.

https://github.com/andrewarchi/ws-challenges

To see if gojq works even with complex jq programs, I tested it on my wsjq[0] Whitespace language interpreter, which uses most of the advanced jq features. It impressively appears to support the full jq language, though I uncovered a bug[1] in gojq.

gojq's arbitrary-precision integer support will be useful (jq just uses 64-bit floating-point), though I suspect it will have performance regressions, since it uses math/big, instead of GMP.

[0]: https://github.com/andrewarchi/wsjq

[1]: https://github.com/itchyny/gojq/issues/186

According to Guinness, the top is Voyager 2:

> The computer system that has been in continual operation for the longest period is the Computer Command System (CCS) onboard NASA's Voyager 2 spacecraft. This pair of interlinked computers have been in operation since the spacecraft's launch on 20 August 1977. As of 29 October 2020, the CCS has been running for 43 years 70 days.

https://www.guinnessworldrecords.com/world-records/635980-lo...

In my fork of the article, I added documentation links and ordered the sections more sensibly: https://github.com/andrewarchi/compiler-notes/blob/main/rust...

> you can use a "folder structure" of tags. You can name tags things like subcomponent/v1.0.2. […] Doing that can confuse git describe

Using the --match option, `git describe --match='subcomponent/*'` fixes this problem. It filters the tags that are considered to only those matching the pattern, so that a later tag for another subcomponent will not be used.

I find the stateless streaming paradigm in jq very pleasing.

Results can be emitted iteratively using generators, which are implemented as tail-recursive streams [0]. Combined with the `input` built-in filter, which yields the next item in the input stream, and jq can handle real-time I/O and function as a more general-purpose programming language.

I built an interpreter for the Whitespace programming language in jq using these concepts and it's easily one of the most complex jq programs out there.

[0]: https://stedolan.github.io/jq/manual/#Generatorsanditerators

[1]: https://github.com/andrewarchi/wsjq

In fact, jq already has `map`, which would replace the article's pattern of `[.[]|add]` with `map(add)`. It is defined as such:

    def map(f): [.[] | f];

Many built-in functions in jq are implemented in jq, in terms of a small set of core primitives. The implementations can be inspected in builtin.jq.

https://github.com/stedolan/jq/blob/master/src/builtin.jq#L3

> Parcel CSS is based on the cssparser[0] Rust crate, a browser-grade CSS tokenizer created by Mozilla and used in Firefox. This provides a solid foundation, including tokenization and basic parsing. However, it does not interpret any CSS properties or at rules. That's where Parcel CSS comes in. It handles parsing each individual rule and property value, as well as minification, compilation, and printing back to CSS.

https://github.com/servo/rust-cssparser

Was this a port of the Flash app or reverse engineering it? The description on GitHub mentions that the Flash version was made by your friend, so I presume you have the original source available.

I've wanted to port an old Flash game for a long time, but I only have the .swf file, not .fla, because I'm not the original developer. I've tried several decompilers to examine the code and resources, but it would take a lot of work to make sense of the obfuscated code. Unfortunately, it can't be played in the Ruffle emulator since it is written in ActionScript 3, which is not currently supported.

I'm solving Advent of Code in Whitespace, a quintessential esolang.

https://github.com/andrewarchi/ws-challenges

Sounds like the Nand to Tetris course, gamified.

https://www.nand2tetris.org/

I implemented a Whitespace interpreter in jq!

https://github.com/andrewarchi/wsjq

What timezone is that? I don’t see it in the tz database.

My favorite may be Lord Howe Island in Australia (Australia/Lord_Howe), which uses +10:30 in the winter and +11:00 in the summer.

> instead of refreshing like a lunatic for new information all the time during your day. You simply search for a solution only when you are experiencing a problem.

> You treat social media like any other website online. You visit it only when you need something. You don’t visit it to find something to need.

Adjacency matrices would make ownership clear and solve the single-writer/multiple-reader issue because nodes wouldn't directly reference each other, but it keeps the exact same relationship between nodes, so any memory leaks are still possible (e.g. not cleaning up dead code because it is cyclic and appears to have references). If I'm going to defeat the type system, it seems like raw pointers would be easier.

I’m in the early stages of working a compiler in Rust and haven’t gotten to the IR infrastructure yet. With Rust’s borrow checker, how can I make the IR graph safe, with its control flow preds and succs and data flow inputs that make it so there isn’t a clear owner for any node. How does rustc do this?

I always find it interesting how frequently Dutch is intelligible, knowing German and some basic sound shifts: „Ihr Gulden ist hier einen Thaler wert“

Nuitka looks like a traditional ahead-of-time compiler using SSA form[0] and is written in Python. I’d be interested in seeing performance comparisons with PyPy, which uses the second Futamura protection and is written in a dialect of Python.

[0]: https://nuitka.net/doc/developer-manual.html#ssa-form-for-nu...

> This was all done within Europe where we have the highest concentration of tor nodes.

So Tor nodes take locality into account? Although, that would improve speeds, it seems like an information leak.

Internet Archive collections are available as web seed torrents and download much faster than over HTTP because multiple servers are used concurrently.