MadMode

Formal Verification is catching up with cutting-edge Mathematics

Wed, 01 Jan 2025 00:00:00 +0000

Formalization has trailed cutting-edge mathematics for some time: the four color theorem was proved in 1976, but it wasn't formally verifed until 2005.

This was one of the objections of the QED manifesto in 1993:

Objection 4. Mechanically checked formality is impossible. There is no evidence that extremely hard proofs can be put into formal form in less than some utterly ridiculous amount of work.

Reply to Objection 4. Based upon discussions with numerous workers in automated reasoning, it is our view that using current proof-checking technology, we can, using a variety of systems and expert users of those systems, check mathematics at within a factor of ten, often much better, of the time it takes a skilled mathematician to write down a proof at the level of an advanced undergraduate textbook. (emphasis mine)

Today I got a github notification that prompted me check in on recent discussion around Metamath, and I learned that one of the greatest living mathematicians is formally verifying his work as he develops it:

... when it comes to formalising mathematics in real time, we now have an even more spectacular data point: Terry Tao led a team which formalised the main result in his breakthrough new paper with Gowers, Green and Manners proving Katalin Marton’s polynomial Freiman-Ruzsa conjecture. The 33 page paper was formalised in just three weeks (before the paper had even been submitted)! -- Lean in 2024 | Xena

My notes show I first looked at Lean back in 2015. I'm trying to remember what I didn't like about it... ah yes... it's written in C++ and the logic is kinda hairy.

The logic does have a kernel, which was written up by someone I recognize from the Metamath community:

Mario Carneiro, 2019. The Type Theory of Lean.
The Type Theory of Lean - YouTube

In his mm0 work, he calls it a "very strong axiomatic framework".

I tried to read that paper; it's a little over my head. But Lean can export proof objects and there are independent checkers. tc.rs is the core of a rust implementation; it's over 1000 LOC; over 5000 if you count the modules it imports. Compare with the 362 line otter proof checker. The Type Checking in Lean 4 docs are just about my speed, though. Thanks!

awesome-ocap stargazers grow steadily since 2017

Thu, 12 Dec 2024 00:00:00 +0000

The number of stars on my awesome-ocap repo has grown steadily since My Capability Security 2017 Wish-List.

My github feed shows new stars now and then, which made me curious about how folks are discovering it. I expected the growth would be episodic -- prompted by events now and then.

The nearly straight line over 7 years is quite a surprise!

TODO: check the linear hypothesis with pandas. Get slope, coefficient.

The web knows how to make this chart

I just wished into a popular LLM:

for my dckc/awesome-ocap github repo, how do I get a chart of when the stargazers arrived? I want to make a chart

and it got script.py right on the 1st try, IIRC.

PyData tool setup: uv beat nix

The LLM's first draft for fetching was some shell code that had a silent endless loop, which put me in rate-limiting penalty box at github. I tried using nix to set up a python env for pandas and such, but the rate limiting put the kibosh on that. So I used uv to manage the dependencies.

I used direnv to manage $GITHUB_TOKEN.

p.s. commit history for the gist:

2024-12-12 00:29 496c37f
2024-12-12 00:27 0d7ec8b
2024-12-09 09:41 035f04b

rebuilding madmode on 11ty using aider

Sat, 28 Sep 2024 00:00:00 +0000

Generative AI can definitely be a productivity booster... "I'm kinda scared of my python site builder now," I wrote way back in 2016. I've been sort of stuck since then.

Then I learned about aider, "pair programming in your terminal". It took just 2 and 1/2 hrs to re-created the features of my blog with modern JavaScript tooling.

After setting up billing, we start start it with aider --sonnet. Then literally type Create an 11ty blog called MadMode with the subtitle "Dan Connolly's hacking notebook". And whoosh:

Not only that, but aider makes a git commit out of what it did. No more copying and pasting code between the LLM chat window and your text editor.

2024-09-21 11:53 850441f feat: Create an 11ty blog called MadMode with the subtitle "Dan Connolly's hacking notebook"

Its first try had a bug. So I typed fix it. And it did.

2024-09-21 11:54 7fc1488 fix: resolve template render error in layout.njk

aider offers to run the command to start the site in dev mode, and I agreed. The initial site looks like this:

Retrofitting the file structure to my existing content is something that usually trips me up when trying to migrate to a different blog engine. It was pretty much automatic with these tools:

2024-09-21 11:57 44d680e feat: move the source of the posts to pages/YYYY

It borked the footer code now and then. I was about to give up in frustration, but since fix it generally works, I just moved on without worrying about it too much.

2024-09-21 12:03 d93752d fix: Remove Liquid escaping from copyright footer

Tags took a couple tries:

2024-09-21 12:07 152ff32 feat: Add 'writing' tag to first post
2024-09-21 12:09 804eb5a feat: Add navigation and improve layout

Between those two, I said I don't see the new "writing" tag. how do tags work in 11ty?

With an LLM, we don't have to settle for Lorem Ipsum. I made a make up a dozen posts going back several years wish, and lo...

2024-09-21 12:12 591e119 feat: Add a dozen new blog posts and update index page with archives

Next wish: under Recent Posts, each item should include the post summary. if the post has no explicit summary, use the 1st 135 characters

2024-09-21 12:35 5123baa feat: Add post summary to Recent Posts section

each post should show the date and tags at the bottom

2024-09-21 12:39 4a9cf7f feat: add date and tags to post layout

add a tag index; that is: a list of the tags, each linked to a list of all the posts with that tag

2024-09-21 12:42 46e57da feat: Add tag index pages

good. but can you change the url structure from /tags/foo/ to /search/label/foo/ ?

2024-09-21 12:43 f9dc1d0 feat: Change URL structure from /tags/foo/ to /search/label/foo/

good! now change the tags index from a list to a tag cloud; that is: tags with more posts are bigger

2024-09-21 12:45 45afb88 feat: Implement tag cloud in tags index

I did a little research to figure out which search library I wanted to use, and then asked it to add search using minisearch:

2024-09-21 13:08 4f8d01b feat: Add search functionality using MiniSearch

Then I started playing around with style:

2024-09-21 13:25 55e0f22 feat: use serif fonts
2024-09-21 13:27 26e7149 feat: Add blockquote styles with italics and large quotation mark
2024-09-21 14:21 6ae305a feat: Add laboratory notebook style to background

And finally:

2024-09-28 03:37 472793c feat: Move the Welcome section to the bottom and rename it to "About MadMode"

move-section-down.cast https://asciinema.org/a/678027

aider wrote 7% of its own code in the most recent release, it wrote 70% https://github.com/paul-gauthier/aider/releases/tag/v0.57.0

It can definitely make something good enough to criticize... not a finished product, but something that's close enough to go "no, not like that, but..." and now you have a better sense of what you do want.

One Year with an E-bike

Sat, 04 May 2024 00:00:00 +0000

I wasn't sure how long it would last when I replaced my car with an ebike. After a year, I have not once wished I had my own car.

When one of my kids moved out last spring, I gave him my car, a 2006 Infinity G35X. Shopping for a replacement was a depressing prospect. I had gotten a great deal on that G35 in 2019 (paid about $5k, including $1.5k in repairs), and I had little hope of finding another deal like that, especially with the impact of the pandemic on car prices.

Retail used-vehicle prices now average $26,510.

With new car prices averaging $49K, I started to think I might as well get a Tesla. But as I looked closer, I realized they're not so good for the planet after all.

Walk, bike or take the train for the lowest footprint -- Our World in Data

With several e-bike models around $1,000, I figured I could hire a car when I need one and still save a lot.

Heybike Ranger

I like the fat tire style. I picked a Heybike Ranger Electric Bike (from amazon).

Assembly took about an hour, with a few frustrations here and there as the instructions and video didn't exactly match what came in the box.

Riding to shops and restaurants

Feeling the wind and sun as I ride to nearby shops and such really is exhilarating.

Full disclosure:

Mine wasn't the only car in the house. I still have access to my wife's car when she is not using it.
I work from home, so commuting is not an issue.

I have some of the usual accessories:

BriskMore Bike Handlebar Mirror
Via Velo Heavy Duty Bicycle U-Lock - the U-Lock is a pretty secure option, except that sometimes I don't bother. Plus, it rattles when I ride. So I'm considering one of the motion-activated alarms.
Lamicall Bike Phone Holder - Google Maps has pretty good bike directions.
ROCKBROS Bike Trunk Bag - I tried a couple different kinds of panniers and even a milk crate. But they get in the way when I'm just trying to get from here to there, and getting them on and off is a bother. So this bag is just right: I keep it on all the time, but I only unfold the panniers when I need them for groceries or the like.

Folding

Lifting the 70lb bike is a bit of a challenge, but folding is especially useful if I bike one way and get a ride the other; it even fits in the back of a Prius!

Brakes: squeaky or mushy

The brakes squeaked when I first got it. I found an adjustment to address that, but it made the brakes so mushy I could hardly stop. So I live with a bit of squeak.

Speed: 25mph

Ok, so it only goes that fast downhill. But even uphill, going 15mph+ without pedaling hard sure is nice :)

The top speed is fast enough that my eyes water. So rather than one of the bike helmets we've had in the garage for decades, I now use a VICTGOAL Bike Helmet with Detachable Magnetic Goggles. Bonus: works as sunglasses too.

Cold weather riding

Going that fast does make it feel colder. But with the right gear, even riding below freezing is not bad. LINGSFIRE Bike Handlebar Mittens are cozy.

I haven't tried it in the rain, much.

Range?

I don't know what the range is. My trips are typically a mile or two. I averaged 7.7miles per week over the year. I think my longest trip was about 5 miles each way. It was to music practice, with my guitar on my back :)

Ubuntu 5.10, archive.org, and .torrent files

Thu, 21 Dec 2023 00:00:00 +0000

I'm ready to say goodbye to my copy of Ubuntu 5.10 for i386 on CD, after nearly 2 decades of keeping it as a combination keepsake and software supply chain anchor. I donated it to archive.org:

While brainstorming about Merkle trees for file access, I noticed that not only does archive.org OCR the PDF I gave them of the cover and support browsing of the contents of Ubuntu 5.10 i386.iso, but they provide ubuntu-5.10-pc_archive.torrent, which means I can have high-performance access to the the full contents of the CDs for just 29k of storage. And brave supports .torrent files natively with WebTorrent (WebTorrent Tutorial looks pretty straightforward.)

But what's in that .torrent file? Aha! bencode from BEP 3! I've heard of it in OCapN discussion but didn't realize it comes from bittorrent. BitTorrent bencode format tools is really handy, including stopping in a debugger to see the details:

BCode.hs from haskell-torrent has a crisp specification:

-- | BCode represents the structure of a bencoded file
data BCode = BInt Integer                       -- ^ An integer
           | BString B.ByteString               -- ^ A string of bytes
           | BArray [BCode]                     -- ^ An array
           | BDict (M.Map B.ByteString BCode)   -- ^ A key, value map
  deriving (Show, Eq)

...

-- | Return the hash of the info-dict in a torrent file
hashInfoDict :: BCode -> IO Digest
hashInfoDict bc =
  do ih <- case info bc of
              Nothing -> fail "Could not find infoHash"
              Just x  -> return x
     let encoded = encode ih
     digest $ L.fromChunks $ [encoded]

Playing with parse-torrent in a parse-torrent-ubuntu-5.10 project on StackBlitz is handy in that it shows the infoHash, b890d2e1174a809d1cd0437de30400c542e0a939, but its JSON output misled me about the real structure: there is no infoHash key in the file; there's an info dictionary that gets hashed.

Say... Ubuntu offers bittorrent as a download option; maybe they keep a 5.10 .torrent file around? I didn't find one from them, but I did find:

Ubuntu 5.10 (Breezy Badger) : Canonical Ltd., Ubuntu community : Internet Archive
Source torrent:urn:sha1:329a357ebd51db73417e1ad767b041291f598ae8 Addeddate: 2017-06-20 14:16:31 Identifier: Ubuntu-5.10

Note the Source; yes, Internet Archive ingests BitTorrents.

Somehow my Ubuntu 5.10 i386.iso is 632,262 kb, which is 300 kb larger than theirs (631,962 kb). Maybe some unused space captured by gnome-disk-utility when I ripped the CD?

walk-n-talk?

Sat, 18 Nov 2023 00:00:00 +0000

walk-n-talk?

That's short for: would you like to talk with me as I take my dog on a walk?

When the pandemic hit, I traded in my commute to KU Med Center for a walk with my dog Mojo.

While we're out walking, I like to talk with a friend, family member, or some colleagues. Mojo really likes it because I lose track of time and she gets to smell everything more.

Usually it's a plain 1-1 phone call (or signal call). But sometiems it's a group thing. It's great to talk-real time with colleagues around the globe, but sometimes the tech reminds you that there's nothing like being there:

Zoom: the dominant player. Pretty reliable
Jitsi Meet: based on open tech. Also reliable in my experience. The main drawback is that recording isn't as well integrated.
Discord void: disappointing, especially since I gather the reason it was created was to provide a voice side-channel for gaming.

Contact me if you're interested to chat some time.

Office Hours: Patterns of Cooperation without Vulnerability

Sat, 18 Nov 2023 00:00:00 +0000

One of my favorite patterns of cooperation is Office Hours. I open my office, virtually, and welcome questions and other open discussion, mostly about the way object capabilities can be used to form patterns of cooperation without vulnerabilities, but also wider discussion of Web Architecture, open source, project management... and occasionally, to fill gaps, guitar :)

Agoric Dev Office Hours on Wednesdays is the main series these days.

Notes with video recordings are the norm. All episodes have at least a tab dump of the links discussed in the session (thanks to the TabCopy extension).

There's a lot going on at Agoric!

Big News at Agoric: AppJam at Cosmoverse, Liquid Staked ATOM for Vaults - Agoric Community Forum Oct 15

I started doing Saturday RChain community building office hours: Story Telling and Test Cases in 2018. but as the RChain Blues set in, I re-scoped my Saturday time as awesome-ocap office hours.

I haven't had critical mass on a Saturday morning for a while, so I join Hack & Craft now and then. Darn... this is an off week; they only run 1st and 3rd Saturdays of the month.

Toward capabilities all the way down with Genode on a Thinkpad

Tue, 03 Jan 2023 00:00:00 +0000

In this year's holiday lull, I got closer to a "capabilities all the way down" workstation using Genode, an OS framework with capability-based security.

Sculpt is a Genode-based general-purpose OS.

Genode has a choice of low level microkernels at the bottom. Sculpt uses the NOVA microhypervisor:

... the NOVA microhypervisor uses a capability-based authorization model and provides only basic mechanisms for virtualization, spatial and temporal separation, scheduling, communication, and management of platform resources.

NOVA isn't formally verified like seL4, but it's tiny (9,000 LOC):

Figure 1: Comparison of the TCB size of virtual environments. -- Steinberg 2010

... not to mention mature: that peer-reviewed release was in 2010 and the spec last changed in 2014. It's clearly trustworthy enough for my hobby usage.

For reference, genode sculpt-22.10 ports/nova.port points to NOVA a34076e, modified Sep 29. So they do continue to make the occasional tweak here and there to the C++ code... prompted by Sculpt usage, I suspect.

The Sculpt release notes include a tutorial on how to boot it from a USB drive and play around with it; I managed to get that far back in 2018. This time, I got a more clear understanding of how persistent configuration on a partition of the USB drive works. A big clue is that the built-in "inspect" view is plenty for command-line file manipulation; there's no need to install and configure all the components of a shell.

I wanted to reproduce Schlatow's results from Starting an existing Linux installation from Sculpt. I managed to

partition the hard drive
- considered nix declarative disk partitioning with disko a la McGee's notes
  - learned a bit more about nix flakes
  - tried to make my own flake; re-discovered my problem with nix: unlike apt where if you get an option wrong, some C code tells you that you got an option wrong, nix just passes the wrong option down into interpreted code where you eventually get “string found where integer expected” or some such. As Phil Karlton would say, "yet another interpreted language without a debugger."
install linux on the internal SDD
install genode on another partition
- though I couldn't get the grub config to work automatically

and I downloaded the components to run a VM, but when I tried to start it up, it couldn't find /machine.vbox6:

[runtime] child "vbox6"
[runtime]   RAM quota:  4402952K
[runtime]   cap quota:  7966
...
[runtime -> vbox6 -> vbox] main     Executable:  /virtualbox6
[runtime -> vbox6 -> vbox] Error: failed to init machine from settings
[runtime -> vbox6 -> vbox] Runtime error opening '/machine.vbox6' for reading: -102 (File not found.).
[runtime -> vbox6 -> vbox] /data/depot/genodelabs/src/vbox6/2022-10-11/src/virtualbox6/src/VBox/Main/src-server/MachineImpl.cpp[499] (nsresult Machine::initFromSettings(VirtualBox*, const com::Utf8Str&, const com::Guid*))
[core] attempted exec at non-executable memory (EXEC pf_addr=0x271dd78 pf_ip=0x271dd78 from pager_object: pd='init -> runtime -> vbox6 -> vbox' thread='ep') 
[core] page fault, pd='init -> runtime -> vbox6 -> vbox' thread='ep' cpu=0 ip=0x271dd78 address=0x271dd78 stack pointer=0x403fe6b8 qualifiers=0x15 IrUwP reason=3
[core] no RM attachment (READ pf_addr=0x0 pf_ip=0x16bb302 from pager_object: pd='init -> runtime -> vbox6 -> vbox' thread='Watcher') 
[core] page fault, pd='init -> runtime -> vbox6 -> vbox' thread='Watcher' cpu=0 ip=0x16bb302 address=0x0 stack pointer=0x409feb00 qualifiers=0x4 irUwp reason=1

After a a bit of diigoing, I came to the conclusion that there's a significant gap in my education around using VirtualBox in general, never mind in Genode.

Divesting from Flickr in the Annual File Purge

Tue, 03 Jan 2023 00:00:00 +0000

I spent much of this year's annual file purge recovering from Flickr going back on their 1TB storage offer.

While tinkering with Genode and catching up on Metamath (RIP, Norm Megill), I made a lot of use of github issues as my lab notebook; I can search copies of my comments in my email since I'm a closet librarian and I don't trust cloud services completely. One of these searches led me to the pile of monthly "account in violation free account limits" nasty-grams building up since May:

Update: Free account limit changes and enforcement start May 1, 2022. \| Flickr Blog

Back in 2015, I mostly knew better, but I did take them up on their terabyte storage offer:

My photostream on flickr goes back to Dec 2004 when it was big in the open web community. I could never bring myself to go premium, but in May 2013 when they announced the terabyte storage offer, I dusted it off. - MadMode: Syncing a 5 Year iPhoto Library with flickr

I have about 50GB of files from a Flickr data request Feb 17, 2019 on an external SSD. I didn't take the time to keep the private data separate from the code and other detailed notes, but briefly, I

verified access to 47GB of data from a March 2019 Flickr data request (72157706876334384_ff8f2206a90f_part1.zip etc.) by copying it from an external SSD to an internal NVMe.
- Why did that take 20 minutes? Oops... I used a USB2 cable and so lost USB3 "SuperSpeed"
verified that I can recover a favorite album from iPhoto
- dealt with the fact that the photo_NNN.json files don't actually contain the name of the abc_NNN_xyz.jpg media files
- joined the flickr ids with iPhoto ids using records from the 2015 upload process
  - used nix to bring up a juypter notebook environment with the relevant goodies: nix-shell -p "python3.withPackages(ps: with ps; [ipython jupyter numpy pandas pillow flickrapi progress crc32c])"
- made a simple HTML list of links to photos
- reverse-engineered the way Web-iPhoto would make an album of those photos from iPhoto files:
  - wrote out albums and photos JSON
    - discovered the README docs were incomplete and the code needs tree too.
verified that I can recover a favorite keyword from Apple photos
- reified the keyword as a directory with symlinks to the relevant photo files
- toured simonwillison's dogsheep-photos work and osxphotos while decoding the Apple photos database.
- evaluated photoprism, an "AI-Powered Photos App for the Decentralized Web" in hopes that open source AI would help me curate interesting photos the way Apple's applied computer-vision research did for Simon
  - wow! nicely packaged!
  - bulk import with move option for canonical naming: 2015/10/20150510_015146_88F59DFB.jpg
    - that hash is a Castagnoli crc32c, the one with hardware support, not the one from the python stdlib.
deleted all 10,000+ non-private photos using the flickr API so I'll stop getting those monthly nasty-grams.
- learned to use the progress package to see that it would take about an hour

I made lots of diigo bookmarks and annotations too.

Footnote on Apple photos dates

Apple support discussion Apr 2015 gives us some clues about the database schema, which seems to be an Aperture database (apdb).

Aperture uses Core Data, which is a database-independent abstraction layer, and thus does not use the native SQLite encoding for dates (juliandate), but rather the NSDate format, which should be a double-precision number of seconds since the reference date (2001-01-01 00:00:00 GMT). -- majid 2011-05-03

Unbelievably good noise cancellation

Fri, 09 Sep 2022 00:00:00 +0000

It was loud. I mean really loud. Like guns going off over my head. The noise from the nailguns and hammers from the hardwood floor installation going on right above my office.

I apologized to the other folks in the meeting about the background noise, but since my business in the meeting was urgent and the noise wasn't going to get any better, I pressed on.

They dind't hear it. At all. They reported my voice was coming through just fine.

I still hardly believe it.

Hats off to Corsair!

And thanks, B!

$ lsusb | grep -i headset
Bus 001 Device 018: ID 1b1c:0a17 Corsair Corsair VOID PRO USB Gaming Headset

Hello Spritely Institute! And Haunt. And Guix, again

Sat, 08 Jan 2022 00:00:00 +0000

Hello, Spritely Institute!

... ActivityPub, social networks, smart contracts, object capabilities, and secure distributed virtual worlds. ... freely licensed open source ...

Yum, yum, gimme some! Can't wait for mind-boggling stuff like this VRChat hack, but powered by ocaps and open source!

Privacy & moderation issues have triggered the permanent shutdown of millions of networked communities and the destruction of their relationships and artifacts.

I was just talking with @simonw about portable posts using ERTP. More on that later...

Nice site btw... shiny!

Powered by Haunt.

Keep talking... looks clean...

gives authors the ability to treat websites as Scheme programs.

Or maybe Scheme programs that are also Hardened JavaScript programs, using James / Jessie on rockit?

Let's give it a spin as-is before stretching it...

To install Haunt ..., run: guix install haunt

Ah yes... guix for ocaps at the systemd level is on my wish-list too. I have guix on my Ubuntu workstation, don't I? Let's see... guix install haunt... bingo!

Catching up with Guix after 55 days

meanwhile...

guix install: warning: Your Guix installation is 55 days old.
guix install: warning: Consider running 'guix pull' followed by
'guix package -u' to get up-to-date packages and security updates.

so...

15:38 jambox$ guix pull
Updating channel 'guix' from Git repository at 'https://git.savannah.gnu.org/git/guix.git'...
Authenticating channel 'guix', commits 9edb3f6 to 2dfbd03 (5,405 new commits)...
...

Ugh... taking a while... I wonder what it's doing, so I hop over to #guix and learn that the 5K commits include a big merge recently. I'm just about to give up on it when it comes back to life...

185.4 MB will be downloaded
building /gnu/store/7y8wijc8zmbf8il1yzrv4ivmggi5zx7i-compute-guix-derivation.drv...
Computing Guix derivation for 'x86_64-linux'...

News for channel 'guix'
  Icedove 91: profile folder moved to `~/.thunderbird'
  `gdm-service-type' now supports Wayland

16:10 jambox$ guix package -u
The following derivation will be built:
   /gnu/store/gpf86rpdl5k21v65xdshv7qdypwc3w89-profile.drv
33.2 MB will be downloaded

16:15 jambox$ guix install haunt
The following derivation will be built:
   /gnu/store/kciishw2a3xb52ql3m55m3g16dry7p0h-profile.drv

Thansk for the "News..." bit. The editorial discretion shows user-centered design. guix search is another breath of fresh air in contrast to the way apt and nix seem to grudgingly provide a search feature. Likewise:

hint: Consider setting the necessary environment variables by running:

     GUIX_PROFILE="/home/connolly/.guix-profile"
     . "$GUIX_PROFILE/etc/profile

guix install emacs gives 27.2 (2021) where Ubuntu gives 26.3 (2019). And guix install gnucash has the new sqlite3 and postgres support. Yes, this could be my tribe. I can't go all in yet because I use Brave and I think there's a reason guix doesn't support it.

Now let's pop back...

Blogging with Haunt eval, cont.

Stubbed my toe on ERROR: In procedure setlocale: Invalid argument. But guix search locale guided me nicely to guix install glibc-locales. Then asset processing failed with errno: "images" 2 because the homepage has (static-directory "images") in the example config but neglects mkdir images. (The tutorial doesn't have this bug.) Now we're rolling:

09:48 connolly@jambox$ haunt serve
serving site on port 8080

So close! If it were serving site on http://localhost:8080 I could just follow the link.

First post! by Eva Luator

There's my tribe again :)

But I doubt netlify supports guix as well as they support python and node.js. Here's hoping they do it well enough...

Closet Librarian Approach to Cloud Services

Sat, 18 Dec 2021 00:00:00 +0000

A colleague suggested we shouldn't delete calendar items of old meetings. I said I don't rely on my calendar for records of the past. Then I admitted that actually, I keep version-controlled backups of my cloud-hosted calendars.

I'm content to use the Google calendar export feature manually. I tend to do it in preparation for travel or perhaps when reviewing a trip:

gdata$ hg log10
790:9efa3d723bb1 2021-10-16 before SFO trip
789:03f577c7a24e 2021-08-08 RedRocks Road Trip KML data from Google Timeline

In general, I don't trust any cloud services. I keep backups of linkedin contacts, tweets, etc.

I'm much more comfortable using github issues to capture my thoughts since I discovered "Include your own updates" in the email notification settings.

I generally follow the IndieWeb PESOS pattern: Publish Elsewhere, Syndicate (to your) Own Site rather than POSSE: Publish (on your) Own Site, Syndicate Elsewhere. The cost of keeping backups in an open format is manageable (I avoid services that don't support it) but economies of scale naturally result in rich knowledge capture and sharing user interfaces for large communities--why should I limit myself to the writing tools I can maintain on my own site?

The ownership risk seems manageable: in large communities including many of my peers, I rely on them to alert me to poor terms of service, and when I venture out on new ground, I read the TOS myself fairly carefully.

PESOS also gives me editorial discretion over which syndicated copies go on the front page of my blog and which go on backups in a closet.

What's Next: Agoric Computing

Mon, 11 Jan 2021 00:00:00 +0000

After 15 years at W3C and 10 years at KU Med Center, my next gig is at Agoric. Here I answer some questions, some recently asked and some anticipated.

Q: I see a NY Times feature about Tim Berners Lee and his new company, Inrupt. Did you work with Tim Berners-Lee?
A: yes, from the early 1990s to 2010 we worked together building the Web at W3C.

Q: Are you working with Tim at Inrupt?
A: No, but I am starting a new job at Agoric.

Q: What is Agoric? What do they do?
A: Agoric provides a safer, simpler way to program smart contracts. We believe smart contracts enable the future of global economic cooperation.

Q: Why is it called "Agoric"?
A: Agoric stems from agora, the Greek term for a meeting and market place. An agoric system is a software system using market mechanisms. (Miller and Drexler, 1988)

Q: Smart contracts? What's that?
A: If you've used amazon, ebay, or a vending machine, you've used a smart contract: a contract-like arrangement expressed in software, where the behavior of the software enforces the terms of the contract.

At W3C, a big part of my job was developing the W3C standards process and figuring out how much of it could and should automate; looking back, I think of it as smart contract design.

Q: Are these smart contracts for blockchains and cryptocurrencies like Bitcoin and Ethereum?
A: Yes, Agoric plans to build on the high-integrity shared compute infrastructure provided by blockchains, though the architecture scales down to private clusters and single machines as well. (Miller, 2019)

Agoric is not building on Bitcoin or Ethereum directly, but we are building on mature blockchain technology, the Cosmos SDK. In order to bridge to Ethereum and Bitcoin, Agoric is a leading contributor to IBC, the Inter-Blockchain Communication protocol.

Q: How are smart contracts safer using Agoric's technology?
A: At least three ways:

Agoric provides offer safety: when you place an offer, either you'll get what you wanted or you get a refund, regardless of the (mis)behavior of the underlying smart contract. This API (Zoe) is built using a couple of more fundamental mechanisms:
Agoric supports patterns of cooperation without vulnerability using object capabilities (OCaps).
Agoric avoids reentrancy hazards (such as the $50M DAO bug) using asynchronous eventual-sends.

Q: Do developers have to learn a new programming language to get all this?
A: No; Agoric smart contracts are written in a secure subset of JavaScript that mostly involves sticking to established best practices.

Q: Object capabilities? What's that?
A: Capability-based security is like the way we control access to our cars: I use a key to drive my car. I can delegate driving the car to you by handing you the key. But keys are impractical to forge, so effectively, unauthorized people can't drive it.

In contrast, the traditional way to control access to computing resources is with access control lists (ACLs): each file or database table has a list of who can read and write it. If cars worked this way, the car would let me drive it only if I present the right driver's license; perhaps my wife would be on the list too. But if I wanted to delegate to you, I'd have to update the list of drivers in the car. And what if my son got hurt and I wasn't around to update the list of drivers so his friend could get him to the doctor? (Stiegler, 2004)

Valet parking would be pretty tedious. And the trunk would have to have a separate access control list to do what valet keys do.

Worse: what we normally do when we run programs on our computers is like giving my driver's license to you or the valet to let you drive the car. I have to run the risk that you'll do other things with the driver's license like open a bank account in my name. Maybe I trust you not to do that, but every program on my computer can do anything I can do, including mess up all my files and demand a ransom to get them back. And with our computers connected to millions of other computers via the Internet, we're vulnerable to more than just our friends. With capabilities, making things like valet keys is easy so that each program, and each part of a program, gets access to only what it needs in order to do its job; capabilities support the principle of least authority much better than access control lists. (Close, 2009)

I have been excited about capability-based security since 2001 when I discovered OCaps and composable smart contracts(Miller, Morningstar, Frantz, 2000). Since 2010 I have been responsible for the security of a million or so health records in a clinical data research warehouse at KU Med Center. Being constrained to use ACL-based filesystems, databases, and web applictions drives me crazy! The chance to work on smart contracts with OCaps as a day job is a dream come true.

Q: And Berners-Lee's Inrupt? What do they do?
A: Inrupt "aims to reset the balance of power on the web" by giving users control of their data in "pods," personal online data stores. "Each person could control his or her own data — websites visited, credit card purchases, workout routines, music streamed — in an individual data safe, typically a sliver of server space" (NY Times Jan 10). It uses SOLID, a set of open technologies.

Q: What do you think of Inrupt and SOLID?
A: I certainly agree when Tim says that "too much power and too much personal data reside with the tech giants like Google and Facebook". But

SOLID Web Access Control (WAC) uses ACLs, not capabilities.
I don't see an integrated economic model in SOLID.

To free users from Google, we have to provide the same sub-second search for all of their email, and I don't see how to do that without bringing the application code to where the data is. We're going to want mash-ups of multiple applications. We need the kind of cooperation without vulnerability that only capability-based security brings. I wonder what would happen if we mixed the Agoric platform's ability to scale down to clusters and single machines with the notion of a SOLID pod.

In 2005, I learned that Internet pioneer Dave Clark took a year off to study economics. Since then it has been pretty clear to me that whatever comes next in the architecture of the Internet and the Web, economics needs to be an integral part of the protocols. Bitcoin came along in 2008 and Ethereum in 2014. Mixing in economics increases the motivation for fraud, which has made me hesitant to commit to the cryptocurrency industry as a career. But the Agoric platform provides an increasing level of safety and most of the team has been working on smart contracts with capability security as long as I've been working on the Web, so I just can't pass up the opportunity to join them as they scale it up to global economic cooperation.

Fun with @ski at Agoric "Hack the Orb"

Mon, 07 Dec 2020 00:00:00 +0000

This was great fun... especially working with @suhailski. https://t.co/11uJri3Wvv
— Dan Connolly (@dckc) December 7, 2020

@agoric · Dec 7

2/ 📽️ Umqhele: @dckc, @suhailski, and @tgrecojs built a #dapp that allows you to auction and trade #NFTs that grant access to live video streams. This dapp demonstrates Agoric contract composition, offer safety, and object capabilities. https://github.com/ski/umqhele

3:33 PM · Dec 7, 2020·Twitter Web App

Suhail Manzoor @suhailski · Dec 7 Replying to @dckc
The pleasure was all mine Dan :)

dckc/umqhele 20cdf68 on Nov 23 forked form ski/umqhele

Hack the Orb: the Agoric and Chainlink Hackathon November 6 - 21, 2020

Agoric Monthly Community Call #3 2020-12-02

Relevant people

Dan Connolly @dckc writing software to support health research; using capability security whenever I can
Suhail Manzoor @suhailski A cultural refugee in Edinburgh who is still trying to search and sort his way through life. Retweets are often endorsement but sometimes not.
Agoric @agoric We believe smart contracts enable the future of global economic cooperation. Agoric provides a safer, simpler way to program smart contracts.

Javascript on genode, genode on HP Envy 15

Sun, 07 Jun 2020 00:00:00 +0000

Genode is a microkernel operating system with capability-based security; in the 20.05 release they added capability-based security using seccomp on Linux. That got me excited enough to make some real progress on JavaScript on Genode using the Moddable XS engine and on Genode on an HP Envy laptop.

In genode-js-xs I got this JavaScript code running on genode:

export default function main() {
    let message = "Hello, world - sample";
    trace(message + "\n");
}

It works like this, once it's built (see below):

goa-hello$ goa run
[goa-hello:make] recursive make: make
Genode 20.02-1-gac1b2ec24e
17592186044415 MiB RAM and 8997 caps assigned to init
[init -> goa-hello] Hello before libc
[init -> goa-hello] hello via stdio
[init -> goa-hello] Hello in libc
[init -> goa-hello] lin_xs_cli: loading top-level main.js
[init -> goa-hello]  lin_xs_cli: loaded
[init -> goa-hello] lin_xs_cli: invoking main(argv)
[init -> goa-hello] Hello, world - sample
[init -> goa-hello] main() returned immediate value (not a promise). exiting
[init -> goa-hello] Warning: rtc not configured, returning 0
Warning: blocking canceled in entrypoint constructor
[init] child "goa-hello" exited with exit value 0

I started with the hello package from then Nov 2019 article introducing goa.

Then I grabbed the helloworld example from the Moddable XS SDK, generated C sources, and got it to build.

Then I worked out getting goa run to work. My artifacts is a bit of a kludge: it reaches out from var/build back to src/bin.

before `goa build`: `gensrc`, `genode_platform`

There's a bit of an impedence mismatch between goa build and the Moddable SDK, so use make -C src gensrc to generate C etc. before running goa build.

We also extend the Moddable SDK to add a genode platform using make -C src genode_platform.

Next Steps

event loop: Figure out how to integrate the port of glib to genode to turn the event loop, which is currently commented out, back on.
nix and dhall: Compare goa to genodepkgs

NixOS 20.03 and Genode Sculpt 20.02 on the HP Envy 15

When my son upgraded his gaming laptop last year, I got his hand-me-down HP ENVY 15z-j100 and tried to boot it from free software. I got Windows so messed up that it could neither boot nor repair itself, so I set it aside in frustration.

Prompted by my success with js on genode, I tried a Ubuntu 20.04 USB stick (that I had made for my other son, who uses linux for his gaming PC) and lo, it worked the first time. Ubuntu has gone to the trouble to get their installation media working with secure boot.

secure boot for NixOS looks really bleeding edge, but with a better understanding based on EFI Boot Loaders for Linux: Dealing with Secure Boot by Rod Smith, I managed to turn secure boot off and get NixOS installed.

With all this momentum, I did not give up when booting Sculpt OS 20.02 quit with a just screen full of (?)s. They only document support for Intel CPUs and this has an AMD A10-5750M, so it looked like an AHCI driver problem or some such. But the screen wasn't locked altogether. It responded to enter and to clear... aha! It's a grub prompt with a missing font. terminal_output console dealt with the font issue and the solution turned out to be changing hd0 to hd1 in a grub config file. Genode has no ath9k driver, so wifi isn't working, but I have plenty of ethernet ports and cables. :)

Rosetta Stone: Taking propositions-as-types to the next level

Sat, 02 May 2020 00:00:00 +0000

I read CS papers by turning notation into (@idrislang) code. Slow going, but the only way I really grok. e.g. https://t.co/8Y34KMgiXd more: https://t.co/AecWRmyFJG
— Dan Connolly (@dckc) February 19, 2020

The Rosetta Stone paper by Baez and Stay has been on my to-read list since a conversation with Stay on a bus a few years ago. The scope is a bit intimidating:

Table 1: The Rosetta Stone (pocket version)
Category Theory	Physics	Topology	Logic	Computation
object	system	manifold	proposition	data type
morphism	process	cobordism	proof	program

But in Fun with Categories, the Statebox folks laid the groundwork for grokking category theory with idris in their idris-ct library.

And the RChain community includes a #computational-calculi channel where people get together to study such things... I get to fill in gaps from skipping grad school without all the tuition and tests :). Jake and several other people there immediately agreed when I suggested we read this paper together. Jake dug up Mike Stay's slides and notes and it took just a little work to get the details into the calendar. Jake connected us to the statebox folks via a Category Theory chat group started by Christian W.

Quantum Physics Gap

Of the five domains in the Rosetta Stone, Quantum Physics is definitely the most indimidating, to me. The Quantum Physics Sequence by Yudkowsky in 2008 is the closest thing I have found so far to something my speed, but I think I made it only 1/3rd of the way thru.

I had to look up Hilbert space; fortunately my linear algebra and topology is fresh enough that "a real or complex inner product space that is also a complete metric space with respect to the distance function induced by the inner product" only took a few minutes to grok.

I just watched a lecture by Edward Witten about knots and QM, a recommended Tomaslov passed along from Greg. Quantifier noted A Quantum Mechanics Primer by D.T.Gillespie as highly regarded. Jake sai Baez has a good list of recommend resources.

Fab from Statebox recommended Picturing Quantum Processes. Here's hoping...

Intro to Idris

I gave an intro to idris this week:

Idris is a programming language designed to encourage Type-Driven Development.

In type-driven development, types are tools for constructing programs. We treat the type as the plan for a program, and use the compiler and type checker as our assistant, guiding us to a complete program that satisfies the type. The more expressive the type is that we give up front, the more confidence we can have that the resulting program will be correct.

In Idris, types are first-class constructs in the langauge. This means types can be passed as arguments to functions, and returned from functions just like any other value ...

We have a recording, though it was a pretty informal session.

Installing Idris

Idris docs recommend cabal install idris but that's a pain; nix support for idris reduces installation (and use!) to just[^1]:

$ nix-shell -p 'idrisPackages.with-packages (with idrisPackages; [ contrib pruviloj ])'

I like to combine it with direnv support for nix so that when I cd into an idris project directory, it all Just Works.

[^1]: if you get idris-modules/build-builtin-package.nix:23 is marked as broken, refusing to evaluate, your nix installation may be out of date; nix update-nix worked for me.

There seems to be good vs-code support for idris, but I don't know how to get it to look at the contrib package, so for today, I tried emacs, though even that showed some rough edges.

Formalizing Knowledge with Idris

LaTeX is fine for typesetting knowledge, but my goal is to formalize knowledge such that the machine can help exploit it.

The example I gave in my Feb 29 tweet was a 2016 paper on capabilities and confused deputy attacks.

The first definitions I captured were:

We assume two countable sets, $Loc$ of mutable references and $Prin$ of principals. ... Values consist of integers ($n$), booleans ($tt$, $ff$) and pointers or mutable references $R_r$ and $W_r$.

In idris, this takes the somewhat familiar of a haskell / ML data type:

data Loc = MkLoc Nat
data Prin = MkPrin Nat

data Value =
    IntVal ZZ
  | True
  | False
  | Read Loc
  | Write Loc

This allows the idris compiler to, for example, let me know when I neglected to handle all kinds of Value later in my transcription to code.

Extending idris-ct for the Rosetta Stone

On page 5 of the Rosetta Stone paper we find this nice diagram relating definitions in category theory:

idris-ct already formalizes monoidal categories and symmetric monoidal categories but not closed categories and cartesian categories. Jake started laying the ground work for CartesianCategory.idr and such.

In discussion of cup and cap, Fabrizio answered a question by way of a figure from some of his work on petri nets. He also mentioned Samson Abramsky's work; Computational interpretations of linear logic has been on my list since Greg said it "changed the direction of his career." Here's hoping for time to study that one closely too.

Trying znc IRC bouncer to stay in touch with the ocap community

Fri, 17 Jan 2020 00:00:00 +0000

I'm typically connected to IRC channels for a few ocap projects etc.:

#erights #genode #idris #indieweb #monte #ocaml #sandstorm #swig

I use hexchat to connect to these channels on freenode but netsplits and other failure modes inherent in IRC make for annoying little gaps in the connection from time to time.

An ice storm here in Kansas City gives me a chance to install the znc IRC bouncer in my home office, after a few months of positive experience at work.

Both znc --makeconf and HexChat znc config want me to specify passwords, servers, and channels. I don't have a clear mental model of how it's supposed to work, but I managed to muddle through, I think. Where to back up the config? Passwords don't fit in a dotfiles repo... ok, kbfs += znc-irc-bouncer-config.tgz, hexchat-irc-client-config.tgz.

Toward secure distributed computing with Agoric at SFBW '19

Sun, 03 Nov 2019 00:00:00 +0000

After months of indecision, I decided to go to San Francisco Blockchain Week in hopes of syncing up with the Agoric team. I'm glad I did!

I have been working remotely for a few months on SwingSet on xs:

A key to Agoric's smart contract platform is compatibility between widespread understanding of best practices in JavaScript development with object capabilities and fail-stop deterministic execution. Initial development of cosmic-swingset is based on the popular and feature-rich node.js platform, but node.js represents an uncomfortably large amount of code to include in a trusted computing base as well as a substantial risk to deterministic execution. The xs engine in the Moddable SDK is designed for constrained microcontroller environments. It has some limitations, but the supported feature set seems to be an excellent match for the Agoric platform.

SwingSet has about 500 tests across 15 files. Once I got about 200 in 3 files, I started looking for someone to reproduce my work. Switching from my linux desktop to a macbook for this trip meant I could be that someone. In the Agoric office on Wednesday, I found out that some of the kludges I had put in place weren't portable between linux and macOS, so only about 170 tests are working cross-platform. It was great to be able to chat in person with Brian and Michael about this stuff.

Zoe and Offer Safety

Agoric leveled up their platform this week with Zoe, which provides offer safety: when you place an offer, either you'll get what you wanted or you get a refund, regardless of the (mis)behavior of the underlying smart contract.

For example, autoswap is a cool service, but conventional interfaces provide little assurance as to what is going to happen when you send it some tokens in a transaction. In contrast, a wallet working with Zoe presents offers in an intelligible form and guarantees that the offer is either executed as stated or you get a refund.

There are some rough edges in getting these demos running, but I had done the testnet demo the previous week so it only took me a little chatting with JF and co to get them running.

And the Agoric folks are not alone in smoothing out the UI: Dan Finlay built a MetaMask Agoric Plugin at the DeFi hackathon.

I think it would be fun to formally verify the offer safety property. Mark Miller and I chatted about this with Eric McCarthy, who works on the ACL2 Ethereum project. I have some history with ACL2, and in some sense the untyped style of ACL2 goes well with JavaScript, but I wonder if that's a false economy. I'm more facile with ML style propositions-as-types systems (idris, ocaml) lately.

CESC: Ouroboros, Kara from Oasis Labs, ...

At CESC (crypto economics security conference) Monday and Tuesday, some talks were too full of greek letters for me to follow and others were more like TV commercials than academic contributions. Two that stood were:

Vassilis Zikas on The Evolution of Ouroboros: From Proof of Work to Proof of Stake. He started with an introduction to bitcoin that seemed a little remedial for this venue but he built on the structure of that intro to make a clear presentation of the rest.
Kara from Oasis Labs: privacy-preserving health data analytics. "AI for healthcare is limited by the fact, that the most valuable data is locked in data silos. Kara breaks up these silos and allow researchers to train their models on data that is otherwise hidden from science - extracting value from it, while never exposing the data itself." The talk was a little on the TV commercial side, but the Ekiden on how they mix private compute nodes with the blockchain is pretty convincing. The evaluation includes some machine learning stuff for medical diagnostics.

Epicenter: CasperLabs, Chainlink

I went to the CasperLabs workshop by Michael with Joshy, a fellow rchain expat.

The Chainlink marketplace for connecting smart contracts to real world data sources (oracles) and payment systems looked interesting. I'm a little bummed I missed the chainlink workshop, but I think I made the right call hanging out with the Agoric team instead.

spendr: toward an rchain gRPC client in rust using tokio and async / await

Tue, 10 Sep 2019 00:00:00 +0000

Inspired by mention of a gRPC client and server library in Tokio alpha release with async & await, I tried building an rchain wallet client in rust.

A couple hours later, I had the hello-world client from tower-grpc adapted to talk to the shiny new 0.9.12 release of rnode:

~/projects/spendr$ cargo run
   Compiling spendr v0.1.0 (/home/connolly/projects/spendr)
    Finished dev [unoptimized + debuginfo] target(s) in 3.00s
     Running `target/debug/spendr`
RESPONSE = Response { metadata: MetadataMap { headers: {"content-type": "application/grpc", "grpc-encoding": "identity", "grpc-accept-encoding": "gzip"} }, message: Streaming }

But that client code doesn't use the yummy new async / await stuff. It doesn't look like async / await has made it up to the gRPC level yet. I think I mis-read the blog post; I think it was just saying that tokio has a gRPC client and server library.

Practical production python scripts

Mon, 22 Jul 2019 00:00:00 +0000

In Writing sustainable Python scripts (lobsters discussion), the initial prototype looks like:

import sys
for n in range(int(sys.argv[1]), int(sys.argv[2])):
    if n % 3 == 0 and n % 5 == 0:
        print("fizzbuzz")
    elif n % 3 == 0:
        print("fizz")
    elif n % 5 == 0:
        print("buzz")
    else:
        print(n)

I have a process for turning this sort of thing into production code that I quite enjoy. I just did it for this code in a fizzbuzz.py gist:

1ac9082
621ddad only run when invoked as script
4cfa693 ocap discipline: explicit access to argv, stdout
35e74c6 quick-n-dirty arg parsing
7cfeeea factor out fizzbuzz() from main()
8d85c04 module doctest of usage

The bottom line in the code review checklist in the shop I run is: is this code I would be happy to maintain?

While I appreciate writing documentation first, it usually takes me a few iterations of prototyping before I know what it is I want to document.

I haven't made strict habit of test-driven development, but I do find factoring out tricky bits of logic and adding unit tests for them frees my mind up during development. And I do make it a rule to write tests before fixing any bugs.

Only run when invoked as script

If this code is good, we want to be able to reuse it by importing it from other modules. And even if we never reuse this code, we want the ability to unit test it. So we use the top level convention (if __name__ == "__main__":) to test whether this code is invoked as a script, but we minimize the code there. As a rule, module level code shouldn't do anything but define things:



def main():
    for n in range(int(sys.argv[1]), int(sys.argv[2])):
        if n % 3 == 0 and n % 5 == 0:
            print("fizzbuzz")
        elif n % 3 == 0:
            print("fizz")
        elif n % 5 == 0:
            print("buzz")
        else:
            print(n)


if __name__ == '__main__':
    main()

Ocap discipline: explicit access to IO

To facilitate patterns of cooperation without vulnerability, object capability (ocap) discipline says the only thing globally accessible should be immutable data. This also supports testability. argv and stdout are IO, or at least sources of non-determinism; object capability discipline calls for passing these around explicitly.

Of course we have to get them from somewhere. In an object capability language, they would be passed (directly or indirectly) to main(); we simulate this using _script_io(), a function that we only define and invoke if __name__ == '__main__:


def main(argv, stdout):
    for n in range(int(argv[1]), int(argv[2])):
        if n % 3 == 0 and n % 5 == 0:
            print("fizzbuzz", file=stdout)
        elif n % 3 == 0:
            print("fizz", file=stdout)
        elif n % 5 == 0:
            print("buzz", file=stdout)
        else:
            print(n, file=stdout)


if __name__ == '__main__':
    def _script_io():
        from sys import argv, stdout

        main(argv, stdout)

    _script_io()

Quick-n-dirty arg parsing

The code is now testable, so we start looking inside the functions. Mixing in arg parsing with other logic doesn't smell right:

def main(argv, stdout):
    for n in range(int(argv[1]), int(argv[2]))

For a little script like this, one or two carefully crafted lines is all I'd spend on arg parsing:

 def main(argv, stdout):
    [lo_, hi_] = argv[1:3]
    lo, hi = int(lo_), int(hi_)

    for n in range(lo, hi):
        ...

If we just invoke this script with no args, the resulting traceback is often enough of a usage clue, given that the userbase of these scripts is a handful of devs in the shop (plus jenkins):

$ python3 fizzbuzz.py
Traceback ...
  File "fizzbuzz.py", line 4, in main
    [lo_, hi_] = argv[1:3]
...

For more involved arg parsing, or perhaps if the userbase were larger, I prefer docopt to writing (or worse: reading!) elaborate argparse calls.

Aside: who asked for fizz and buzz to be parameterized?

Parameterizing fizz and buzz adds testing and maintenance burden. Unless we've got a customer requirement, let's skip all that.

Factor out fizzbuzz() from main()

I like to keep our main() functions small and separate logic from IO. Using yield in place of print is particularly convenient. Let's add one quick doctest while we're at it:

def main(argv, stdout):
    [lo_, hi_] = argv[1:3]
    lo, hi = int(lo_), int(hi_)

    for word in fizzbuzz(lo, hi):
        print(word, file=stdout)


def fizzbuzz(lo, hi):
    """
    >>> list(fizzbuzz(1, 6))
    [1, 2, 'fizz', 4, 'buzz']
    """
    for n in range(lo, hi):
        if n % 3 == 0 and n % 5 == 0:
            yield "fizzbuzz"
        elif n % 3 == 0:
            yield "fizz"
        elif n % 5 == 0:
            yield "buzz"
        else:
            yield n

Module doctest of usage

Now we can document and test usage together in the module docstring.

I actually started the module doctest earlier in the process, but I didn't commit it until the end in order to make each commit demonstrate one part of the process.

"""Simple fizzbuzz generator.

The game proceeds with players announcing numbers increasing
sequentially, except for multiples of 3 and 5:

    >>> usage = 'fizzbuzz 1 20'

    >>> from io import StringIO; stdout = StringIO()
    >>> main(usage.split(), stdout)
    >>> print(stdout.getvalue())
    ... #doctest: +ELLIPSIS
    1
    2
    fizz
    4
    buzz
    fizz
    7
    ...
    14
    fizzbuzz
    16
    ...

"""


def main(argv, stdout):
    [lo_, hi_] = argv[1:3]
    lo, hi = int(lo_), int(hi_)

    for word in fizzbuzz(lo, hi):
        print(word, file=stdout)


def fizzbuzz(lo, hi):
    """
    >>> list(fizzbuzz(1, 6))
    [1, 2, 'fizz', 4, 'buzz']
    """
    for n in range(lo, hi):
        if n % 3 == 0 and n % 5 == 0:
            yield "fizzbuzz"
        elif n % 3 == 0:
            yield "fizz"
        elif n % 5 == 0:
            yield "buzz"
        else:
            yield n


if __name__ == '__main__':
    def _script_io():
        from sys import argv, stdout

        main(argv, stdout)

    _script_io()

Reflection

In this example, our 10 line (working!) prototype has turned into 60 lines of code. If a developer asked me to review the original 10 lines after using it succefully for a few days, and if the cost of a failure was just a few minutes, I might not bother to touch it.

But the code did mix IO with logic in a way that makes me uneasy.

More often, the cost of a failure is re-running a Jenkins job that takes hours. And even in early prototype form, scripts are usually longer than 10 lines and applying these techniques turns up a bug or two or at least clarifies the security properties of the code.

And in this case, of the resulting 60 lines:

25 are documentation
- 10 show simulated script output, which is very simple
The main() function is 6 lines that clearly do nothing but parse args, call a function, and output the results
The _script_io() function is formulaic

The fizbuzz() function retains structure of the original 10 line prototype, with just 4 lines added for documentation / testing.

RChain Blues

Wed, 05 Jun 2019 00:00:00 +0000

Working on RChain was fun for a while, but I am no longer be comfortable with the RChain Cooperative's business practices.

I am inclined to keep my distance until I see

quarterly financials on time ("no later than 20 days after the quarter ends" per IOB 1 from the 2018 annual meeting)
the board carry out IOB 4 member participation in governance
timely board agendas and minutes
some details re Barcelona
this open-source cooperative divest any significant interest in a proprietary audio codec license

The story of how RChain's CoinMarketCap rank fell from 30 to over 200 in 2018 would take more energy to tell than I have just now, but to emphasize why something as supposedly mundane as quarterly financial reports has me so uncomfortable...

I assumed since I got involved in Nov 2017 that any organization that had raised $30M from investors would have someone keeping books, so that producing a balance sheets or cashflow statements was a one-click task... I assumed that people were busy and they just hadn't bothered to click that button and share the results.

I should have known this was yet another case where the web reflects reality.

In the board meeting of July 23, 2018, when they decided to spend tens of millions of dollars on a proprietary audio codec, they did not know how much money the coop actually had, according to Meredith at the Oct 2018 annual meeting.

Some new board members were elected and tried to improve corporate governance, but one by one they reached a point of diminishing returns and moved on to other things.

After the April Barcelona incident, one member put it this way:

... it became near impossible to responsibly put one's reputation on the line for this project.

I attempted to steer member engagement in a useful direction in a Special Meeting 19A process; it was a long-shot and not much resulted from it, but I did manage to get over 100 members on record thanking those who had served on the board since the October annual meeting, trying to right the ship:

Whereas Barry Cynamon, Mark Pui, and Kevin Goldstein served with distinction on the RChain Cooperative board, let us thank them for their service.

Migrated from github pages to netlify for continuous deployment, SSL

Thu, 30 May 2019 00:00:00 +0000

A lot of the friction around my blog has been running the build step: re-constituting python dependencies, running the build, manually tweaking the results, and committing the build results to github pages[^1].

pmoorman turned me on to Netlify last fall, so I gave it a try: Holy shnikeys! it worked 1st try with no tweaks whatsoever! I told it my build command was ./site build[^2] and it picked up my requirements.txt, installed the dependencies, built the site and deployed it.

Fiddling with DNS took quite a bit longer, but I got free SSL for my trouble. Netflify pointed out a zillion mixed content issues... enough that I wrote a little fix_insecure.py script to parse their log and make the edits.

While I'm addressing hygene issues, I fixed the dependency vulerabilities that github pointed out.[^3] CONTRIBUTING.md shows how I bootstrap with direnv and pipenv.

[^1]: I migrated from nearlyfreespeech.net to github pages in 2015.

[^2]: When did I switch to frozen flask? Wow... it was 2012. Time flies.

[^3]: Darn. This footnote markup doesn't work because flask-markdown predates deprecating positional arguments.

Smart Contracts for Health Research Data Sharing

Thu, 12 Jul 2018 00:00:00 +0000

I'm under contract with RChain, two days a week from June to December, to work on smart contracts for health research data sharing. I'm still at KUMC for the other three days a week.

RChain Devcon Boulder

In April, I was invited to RChain Devcon in Boulder. I enjoyed Greg's RChain VM talk. (More on that later, I hope.) Vlad's CBC Casper talk was mostly familiar; I think I got most of it from his devcon three talk, which was just my speed.

I gave a short talk about Getting Involved in the RChain Bounty Program (video).

TimBL had written The web is under threat, which I used as a springboard for Can RChain Answer? (video). My summary slide is:

It has a lot of the right pieces:

Object Capability Discipline

Support for Formal Verification

Integrated Economics with Network Architecture

Scalability

Down to transistors

Up to the globe

Visionary Leadership

Cooperative Governance

I did a quick run up of capabilities from simple closure-based objects to sealing and unsealing to capability-based money as in Miller, Morningstar, and Franz from FC 2000, including:

Before presenting the following simple example of capability-based money, we must attempt to head off a confusion this example repeatedly causes. We are not proposing to actually do money this way! A desirable money system must also provide for: ... blinding, non-repudiation, accounting controls, and backing (redeemability).

Then—tada!—I showed that RChain does propose to do money this way by translating the E code to MakeMint.rho:

   contract MakeMint(return) = {
     new pairCh, thisMint, internalMakePurse in {
       MakeBrandPair!(*pairCh) | for(@p <- pairCh) {
       ...

HERON Clinical Data Repository Access Policy

The main smart contract I want to work on is an evolution of the HERON policy enforcement layer, a bunch of python / PHP / SQL code that enforces the policy around access to KUMC's clinical data repository on ~500K patients: you have to be qualified faculty or sponsored by one, and your human subjects training has to be current and you have to sign a couple forms:

Once you get through all that, you can use the i2b2 ad-hoc query interface to do "cohort discovery"; for example, to find out if enough of the right kind of patients come through KU Med for the study you want to do.

i2b2 Harvard Symposium

The i2b2 tranSMART Foundation Harvard Symposium was this year's annual meeting of the i2b2 user community. Automation of regulatory processes is a regular topic and this year John Halamka spoke on Emerging Models of Data Flow - APIs, Blockchain and Cloud. He cut through a lot of the mystery around blockchain technology with a great illustration of one-way hashing. :)

Decentralized identity, verifiable claims

While killing time in the airport, I managed to reach Manu Sporny. His work around verifyable prescriptions has certain parallels with research data sharing. It wasn't all good news, but he did put me in touch with a couple of his colleagues in the Boston area.

I had hoped to meet with Chris Webber and sync up on js libraries for linked data capabilities. Capability security seems necessary and sufficient, to me, for decentralized access control. As Stiegler put it in the picture book:

The patterns described in this picturebook are simple because they discard the modern fascination with the identities of the participants. Individual Authentication is so pervasive, it is now a part of the problem.

Suppose that your car, instead of accepting a delegatable key, demanded that your driver’s license match the car’s title registry, which happens to be in your spouse’s name. Entrepreneurs would leap forward to develop ever more powerful "identity management" for automobiles. We would subcontract to security experts so our teenage daughters could borrow the car to buy milk. Heaven forfend that the daughter, breaking her leg, had to delegate to her best friend to get to the hospital.

Unfortunately, while Chris is closer to Boston these days, he's still a couple hours away.

But I did get to meet Dmitri Zagidulin over breakfast. He has done javascript work both with TimBL and company on solid and with Manu on decentralized identifiers (e.g. did-io). He isn't yet working on linked data capabilities yet, so I twisted his arm in that direction, and away from WebID.

Things started to click for him when I talked about verifyable claims in terms of insurance and markets:

Proof of identity, in so much as it involves revelation of the profile, or enables its revelation through the use of unique identifiers, is trade in an asset when the information revealed is more than the minimum required with current technology. -- Vora et. al from HP at W3C 2001 DRM Workshop

Take proof of age, for example. A smart contract for a client might ask "who will bet me $10 at 50-to-1 that this request comes from someone over 21 years of age?" A business where people are routinely physically present is in a position to take such bets with high confidence.

Personal Health Records

Manu also put me in touch with Adrian Gropper, CTO of Patient Privacy Rights. Meeting in the airport as he was arriving and I was departing was a bit hectic, so I couldn't be sure whether I had read the paper he and Mark Miller worked:

Identity Hubs Capabilities Perspective Rebooting the Web of Trust V, October 13, 2017 by Adrian Gropper, Drummond Reed, Mark S. Miller

His description of HIEofone increased the priority of UMA in my things-to-study-in-more-depth list:

HIE of One (Health Information Exchange of One) is a volunteer-driven open source project to combine emerging standards for access authorization (OpenID HEART) and emerging standards for blockchain-based self-sovereign identity (DID) into a patient-centered health record infrastructure.

He was one of several people on this trip that talked about FHIR deployment in ways that make me want to look into it again. In particular, he mentioned a FHIR sandbox by CMS, the medicare folks.

OCap-safe JavaScript

On the way home, I got stuck in the Washington D.C. airport overnight due to weather. I used the time to start tinyses2rho, some exploratory scala code to integrate TinySES with RChain.

TinySES is a small subset of JavaScript designed so that non-experts can use to write non-trivial non-exploitable smart contracts. It comes from Mark Miller and company, who have been working on object capabilities and smart contracts at least as far back as the early '90s, and recently launched Agoric.

dreaming big at the RChain Governance Forum

Wed, 21 Feb 2018 00:00:00 +0000

I'm back from the RChain Governance Forum in Seattle, which was full of big dreams, just like the first Web conference in Geneva.

Why RChain? Governance and blockchain can't be separated; I felt compelled to connect them. -- Greg Meredith Sep 2017

I went in with almost no idea what that means. But at the closing brunch, I found myself telling the next person at the table that the economics of email—the original decentralized Internet communication platform—was what led me to trade my privacy to Google for spam protection.

Many of us who built the Web had in mind a decentralized system where access to information and freedom of expression would enrich our lives. At some level, we knew sharp tools cut both ways, but ...

When REST was being framed, it seemed inconceivable that two billion people would all agree to use one website (Facebook); -- Fielding et. al. 2017

The result is a vulnerability that Kate Charlet, who worked on Cyber Policy in the U.S. Department of Defense for the last decade, says nation states have successfully used to destabilize our democracy.

Perhaps there's something to all this blockchain stuff; perhaps we can repair the imbalance by integrating economics into the next generation network architecture.

The imbalance in the system has a glib description:

If you are not paying for it, you're not the customer; you're the product being sold. -- blue_beetle Aug 2010

But another way to put it is:

There's a strangle-hold on social media today; people don't get a chance to participate in the economic proposition in an equitable way. -- Greg Meredith, Jan 2017

He emphasizes that we need new ways of coordinating, inspired by resilient living systems and reflective intelligence. Tai Chi on Saturday morning was a whole body experience of it.

And music!

I had great conversations with Peter and Jonathan and Derek and Rudy, including Ted Nelson's ideas on the evolution of movie making.

Greg performed in a group of mind-bogglingly improvisational guitar players. Mostly I felt stressed and out of place when listening to it. But I was right at home when the twelve bar blues chord progression emerged in the middle of it.

I was also pretty much at home when I saw lightning talks on the agenda, so I offered to lead the session. That was great fun. I gave two talks myself and enjoyed a lot of the follow-up discussions.

The technical architecture of RChain also sunk in a bit more. In addition to capability security and namespaces, I'm beginning to see reflection (the R in RChain) as a possible solution to the quoting and diagonalization issues TimBL and I struggled with in the Semantic Web.

References

Fielding, Taylor, Erenkrantz, Gorlick, Whitehead, Khare, Oreizy, Reflections on the REST Architectural Style and “Principled Design of the Modern Web Architecture” ESEC/FSE 2017
- video
Arndt, Verborgh, De Roo, Sun, Mannens, Van De Walle, Semantics of Notation3 Logic: A Solution for Implicit Quantification RuleML 2015
Berners-Lee, Connolly, Kagal, Hendler, and Schraf, N3Logic: A Logical Framework for the World Wide Web Journal of Theory and Practice of Logic Programming (TPLP), Special Issue on Logic Programming and the Web, 2008

Smart Contracts and Capabilities Up Close

Sun, 31 Dec 2017 00:00:00 +0000

This year I was invited to a Blockchain meets Object Capabilities panel in San Francisco July 3 and the RChain developer retreat in Park City Nov 12-17. Leaving Park City was... interesting.

My flight to San Francisco was funded from the $30 that I put into Ethereum in mid 2016--as an educational expense, I thought; I hardly expected to square my investment.

Jorge Lopez of Gravity hosted long-time capabilities leaders Mark Miller, Zooko Wilcox, and Brian Warner as well as Arthur Breitman of Tezos. Zooko also represented Zcash.

Mark Miller with Lopez and Warner to his right and Breitman and Wilcox to his left

Brian gave a great summary of the bitcoin market forces but I was too engrossed in the event to take notes; the one quote I managed to write down was "Satoshi is probably in the room."

Aside: Sandstorm Oasis let me export the grain I took my notes in even though my subscription had lapsed. That's pretty cool.

The evening before the panel, @zooko gave a shout out to my awesome-ocap list, and in a reply from @robertobrien, I discovered RChain's Namespace Logic.

I saw Mike Stay's name, which was familiar from cap-talk discussion, on some of the citations in the RChain Architecture document, and asked him some questions in email. Before long I was contributing little tweaks to the code and wrangled an invitation to the developer retreat.

RChain developer's retreat at Flanagan's pic.twitter.com/5by4odQ85J
— Dan Connolly (@dckc) November 15, 2017

Again, I was too engrossed to take good notes, but they made recordings of the main sessions.

The RChain goals are ambitious, to say the least: "content delivery at the scale of Facebook and transactions at the speed of Visa." Not to mention a an "e pluribus unum 2.0, a new center on a scale-invariant axis reconciling the wisdom of collective and the wisdom of the individual" for collaborating on problems such as global warming. An interview with Greg Meredith from the January RChain announcement filled in a lot of the background for me.

Nash and the gang did an amazing job hosting. We had dinner out most nights and breakfast in the houses in the morning, and it's a tough call which was better.

On the last day, after a mind-blowing week, we were all lounging around, zoned out on our phones, when we noticed the snow. For some, it was their first snowstorm... nice and pretty. Then Nash snapped us out of it: "Get off the mountain now before they close the pass and you miss your flights!" As we were getting in the big rental SUV, I asked, "Have you driven in snow before?" and since she hadn't, the keys passed to me.

The drive out was a little hairy, but Vlad shared some tunes and we all got to know each other a little better.

Escaping Park City

MadMode

Formal Verification is catching up with cutting-edge Mathematics

awesome-ocap stargazers grow steadily since 2017

The web knows how to make this chart

PyData tool setup: uv beat nix

rebuilding madmode on 11ty using aider

One Year with an E-bike

Heybike Ranger

Riding to shops and restaurants

Folding

Brakes: squeaky or mushy

Speed: 25mph

Cold weather riding

Range?

Ubuntu 5.10, archive.org, and .torrent files

walk-n-talk?

Office Hours: Patterns of Cooperation without Vulnerability

Toward capabilities all the way down with Genode on a Thinkpad

Divesting from Flickr in the Annual File Purge

Footnote on Apple photos dates

Unbelievably good noise cancellation

Hello Spritely Institute! And Haunt. And Guix, again

Catching up with Guix after 55 days

Blogging with Haunt eval, cont.

Closet Librarian Approach to Cloud Services

What's Next: Agoric Computing

Fun with @ski at Agoric "Hack the Orb"

Relevant people

Javascript on genode, genode on HP Envy 15

before goa build: gensrc, genode_platform

Next Steps

NixOS 20.03 and Genode Sculpt 20.02 on the HP Envy 15

Rosetta Stone: Taking propositions-as-types to the next level

Quantum Physics Gap

Intro to Idris

Installing Idris

Formalizing Knowledge with Idris

Extending idris-ct for the Rosetta Stone

Trying znc IRC bouncer to stay in touch with the ocap community

Toward secure distributed computing with Agoric at SFBW '19

Zoe and Offer Safety

CESC: Ouroboros, Kara from Oasis Labs, ...

Epicenter: CasperLabs, Chainlink

spendr: toward an rchain gRPC client in rust using tokio and async / await

Practical production python scripts

Only run when invoked as script

Ocap discipline: explicit access to IO

Quick-n-dirty arg parsing

Aside: who asked for fizz and buzz to be parameterized?

Factor out fizzbuzz() from main()

Module doctest of usage

Reflection

RChain Blues

Migrated from github pages to netlify for continuous deployment, SSL

Smart Contracts for Health Research Data Sharing

RChain Devcon Boulder

HERON Clinical Data Repository Access Policy

i2b2 Harvard Symposium

Decentralized identity, verifiable claims

Personal Health Records

OCap-safe JavaScript

dreaming big at the RChain Governance Forum

References

Smart Contracts and Capabilities Up Close

before `goa build`: `gensrc`, `genode_platform`