mekaj

The former may be a means of getting to the latter. I don’t anticipate it will be made illegal without widespread public awareness and disapproval.

By default I’m skeptical of hand-written parsers, especially if they’re implemented in a language lacking memory safety features. I have seen too many parsers fall victim to (domain specific) fuzzing, and the consequences are serious security vulnerabilities.

Parser combinators are great, but they’re still hand-written in excessively powerful languages. That’s error-prone if the goal is to end up with a trustworthy, portable parser. The most frequently used parser combinator tools I know of are embedded DSLs, which means porting such a parser to another language requires manually converting to another parser combinator’s syntax and semantics and potentially implementing a new DSL which hasn’t yet been battle tested.

Parser generators which are in a position to get battle tested by supporting many parser implementations and integrations seem like the safest and most scalable way to go. I’m not familiar with Semantic Designs’ GLR implementation; thanks for mentioning it. Another worth knowing is tree-sitter (https://tree-sitter.github.io/tree-sitter/). As a GLR-based parser generator it supports ambiguous context-free grammars. At first ambiguity may sound like a downside, but without a computer-verified proof that your grammar doesn’t admit multiple valid parses for any inputs it’s safest to assume ambiguity and proceed accordingly. For example, if at parse-time multiple parses are found you have the option to warn the user or even reject their input with a diff of the ASTs so they can try to patch the input so it’s no longer ambiguous.

Tree-sitter is young, but it has reach. Atom editor packages for languages are encouraged to implement tree-sitter parsers. It’s particularly well-suited for editors because it supports incremental parsing. Parsing the same file from scratch after every edit isn’t necessary.

Recently I implemented a tree-sitter grammar for ABNF (https://github.com/jmitchell/tree-sitter-abnf) and an Atom package (https://atom.io/packages/language-abnf) for it. Now I’m exploring how to generate tree-sitter parsers for grammars specified using ABNF, such as Dhall’s (https://github.com/dhall-lang/dhall-lang/blob/master/standar...). My plan is to automatically generate and fuzz C-friendly parser libraries for many languages to make them more accessible. I also want to help address any tree-sitter bugs discovered along the way that could translate into security vulnerabilities in generated parsers. For now this is a labor of love, and I am not affiliated with the tree-sitter project.

There was an incident with similar consequences on April 10, 2014. The cause was a programmed threshold being breached and the impact was 6h of downtime.

Source: "The Coming Software Apocalypse" published by The Atlantic (https://www.theatlantic.com/technology/archive/2017/09/savin...)

walrus01 also linked to https://www.fcc.gov/document/april-2014-multistate-911-outag... in another comment.

The whole series is great! I especially enjoyed _The Reasoned Schemer_ [0] which serves as an introduction to the *kanren languages [1].

[0] https://mitpress.mit.edu/books/reasoned-schemer [1] http://minikanren.org/

I interpreted that option as Keybase needing a local copy of the PGP key. Thanks for helping me understand that's not the case.

I've set up Keybase on my trusted machine with my GPG keypair, and now have a device key on that machine. When I go to Devices -> Add new... -> New Computer in the GUI I'm told to "Type in text code" (along with the note "In the Keybase app on your computer, go to Devices > Add a new device"). I find this confusing because I'm already there. I tried using the only paper key I have, the one corresponding to my first device key, but there's no response when I click Continue. This is the Linux client, by the way. I'm guessing this is a bug, but I'm not sure. Can you confirm this is the same process you went through to generate your second device key?

When I try to log in on the secondary computer, which doesn't have the GPG keypair or a device key, I'm brought to the same error shown in the screenshot.

Thank you and the Keybase team for this. Unlike other services, I think KB has solved the online identity authentication issue.

There's one hurdle I need to work through to get going on chat. Thus far I've avoided uploading my private GPG key to my Keybase profile, or even copying it to other devices (call me paranoid). Unfortunately this apparently means I can't authorize any other devices (see error message: http://imgur.com/a/UOftN). I assumed device keys were meant to solve this problem, but maybe not. Is there a supported way to make a subkey (GPG or otherwise) of my primary private GPG keypair, so other devices can securely authenticate against my KB profile?

EDIT: I haven't yet started using device keys. Maybe they would work?

Trivial, small example: the bug is the prover accepts all inputs.

Find your one true job

This is true and good to keep in mind, but it's also an inescapable risk of any network involving autonomous agents. We're also susceptible to downloading content that's different than advertised (e.g. Rickrolling).

Can you fix the link for the theoretical CS? Currently links to the ML playlist.

Edit: maybe you meant this one: https://www.youtube.com/playlist?list=PLgO7JBj821uHJM__IpdPT...

Depending on the application this may be a reasonable trade-off.

The non-profit Prison Policy Initiative does a lot of research on these issues and petitions the FCC for changes. This page summarizes a lot of their efforts (http://www.prisonpolicy.org/phones/#price). Their other publications are available at http://www.prisonpolicy.org/reports.html

I haven't seen any statements from her, but you can see her body language following the remark (~42:53). Suddenly she stops walking, turns in his direction, her mouth opens wider, she stays frozen there for a brief moment, and then continues walking.

It was named after the protocol: https://github.com/letsencrypt/acme-spec

I wonder if more computer-aided proofs will lead mathematicians to discover serious conflicts in their ontologies. Critical parts of mathematics, and even the way we talk about it, may eventually need to be reworked.

I agree. Somebody from 1915 would already understand the paradigm shift brought by the industrial revolution. The notion of decomposing problems into small, specialized tasks and delegating to people and other resources was familiar.

Consider these technologies and innovations that had already been developed:

* Jacquard loom (http://en.wikipedia.org/wiki/Jacquard_loom)

* Player pianos (http://en.wikipedia.org/wiki/Player_piano)

* Widespread use of interchangeable parts (http://en.wikipedia.org/wiki/Interchangeable_parts#Late_19th...)

* Assembly lines (http://en.wikipedia.org/wiki/Assembly_line)

* Tabulating machine for the 1890 US Census (http://en.wikipedia.org/wiki/Tabulating_machine)

* Transoceanic telegraph networks (http://en.wikipedia.org/wiki/Electrical_telegraph)

* Use of humans for distributed computation (http://en.wikipedia.org/wiki/Human_computer)

Automated computation is an amazing concept, but--at the risk of historic bias--what we have now is merely an optimized and widely available form of what we had then.

What I imagine they'd have a really difficult time accepting is modern physics, particularly quantum theory. Then again, the vast majority of the public today (including me) struggles with it.

Got me intrigued. Here's a link to Bilal's page on the project: http://wafaabilal.com/domestic-tension/

It's not always a mistake. Abstraction has a purpose. The key is using abstractions that are helpful.

Some people find the concision of lambdas helpful, so it's not necessarily a mistake.