keithwinstein

Looks very interesting! We have done a lot with WasmCert-Isabelle (and there's also WasmRef-Isabelle and their 2023 paper, and the earlier WasmCert-Coq); other than being in Lean instead of Isabelle/HOL or Coq, how would you compare the approach you used? E.g. are you able to do an "in-place Store" like WasmRef-Isabelle, and can you represent memories and tables as plain vectors of bytes/refs in memory, can you grow them in-place, etc.? Or any other optimizations/lessons learned?

I'm also curious -- are you just implementing the Wasm binary and text parsing, validation algorithm, and execution semantics in Lean from scratch by reading the English prose in the spec document, and then checking it against the spec tests and the SpecTec description? Or do you have some sort of automated (classical or LLMy) transformation happening? (One could imagine directly transforming the SpecTec, or the OCaml reference interpreter, into Lean... but it sounds like you're not doing that? I think one needs to be a little careful here because e.g. at this point some of the English prose and reference interpreter implementation, and I think maybe some of the tests, are autogenerated from the SpecTec.) Which parts (if any) are outside the scope of the formalization? E.g. for WasmCert-Isabelle, I believe the binary and definitely the text parsing, and I think some of the arithmetic ops, are not covered.

How are you modeling the explicit sources of nondeterminism in the Wasm execution semantics? E.g. NaN representation, {memory., table.}grow, host calls, stack exhaustion, relaxed SIMD instructions, etc., and that's all before we get to the threads proposal? Because if the goal is to prove programs correct, one risk is that I prove my program correct against your Wasm interpreter (which maybe makes certain choices that aren't determined by the spec), and then I run it against another fully-conforming interpreter in the wild and it behaves incorrectly.

Constitutionally, only the federal government is allowed to regulate intellectual property

It turns out that's not exactly the case! See, e.g., Goldstein v. California, 412 U.S. 546 (1973). Before 1978, state (often common law) copyright used to cover a lot of pre-publication works, and until 2018 (when the federal law was amended) state copyright law covered pre-1972 sound recordings, and state copyright still covers obscure things like post-mortem moral rights in visual art or rights to "unfixed" works. See 1 Nimmer on Copyright §§ A.02 & 2.02. Other forms of intellectual property (trade secrets, rights of publicity) remain mostly creatures of state law, and some states also have trademark systems.

For 8-bit, 16 maps to 7.5IRE which is the well understood legal black. Mapping 235 means they mapped peak to 110IRE.

Generally no -- in an 8-bit NTSC-M Rec. 601 system, 16 maps to E'Y = 0 at 7.5 IRE, and 235 maps to E'Y = 1 at 100 IRE. See https://www.poynton.ca/pdf/Poynton-1996-TechIntrDigiVide.pdf

The "16" digital black level is independent of the "7.5 IRE" analog setup. E.g. in Japan with an 8-bit "NTSC-J" Rec. 601 system, my understanding is that 16 still maps to E'Y = 0 which is now at 0 IRE, and 235 is still E'Y = 1 at 100 IRE.

I can't speak to Binaryen, but afaik WABT's wat2wasm and wasm-tools's wat2wasm (aka wasm-tools parse) are both 100% spec-correct in this respect. Parsing the Wasm text format doesn't require any knowledge of the type of each instruction. If you have a counterexample would love to see it!

There are some cool edge cases if you want to print a mismatched multi-value instruction sequence in the folded form (which WABT and wasm-tools again handle "correctly," but not identically to each other, and not particularly meaningfully).

I'm sorry you're going through this! But also a little suspicious because a nearly word-for-word message was posted four days ago on Reddit with some of the details different, including the major and presence of a master's degree, but most of the same phrasing (https://www.reddit.com/r/mit/comments/1q9gdff/unemployed_alm...). If these rants are somehow from the same person (maybe you did both majors and only discussed one in each post?), fair enough and I really am sorry, but I do wonder if we're being experimented upon. :-(

Even more pedantically, “standard time” is not necessarily consistent across each zone (particularly, during the period for which in parts of the zone it is advanced by an hour) since "standard time” only advances for those states, or parts of states, for which an exemption is not in place.

I can't find a source (including 15 U.S.C. § 260a) that supports this reading, although I agree it's a little ambiguous. The law suggests that a region that doesn't observe DST is observing "the standard time otherwise applicable during that period" and is exempt from the provisions regarding advancement, not that "Pacific standard time" depends on where you are (see 15 U.S.C. § 263).

So, the Unix-y convention [] is the simplest way

No argument there!

If we're being really pedantic, in the U.S. context the zones observe "standard time" all year. "Standard time" refers to the standardization across the zone, and the practice of advancing the clock during daylight-saving time changes each zone's standard time. The Unix-style usage of "EST" vs. "EDT" isn't pedantically correct (e.g., New York observes "eastern standard time" even in summer).

See 15 U.S.C. §§ 260a & 263 (https://www.law.cornell.edu/uscode/text/15/chapter-6/subchap...).

Shades of https://www.theregister.com/2006/03/24/tuttle_centos/ (from simpler times, almost 20 years ago!)

This story has been reposted many times, and I think GJS's remarks (as recorded by Andy Wingo) are super-interesting as always, but this is really not a great account of "why MIT switched from Scheme to Python."

Source: I worked with GJS (I also know Alexey and have met Andy Wingo), and I took 6.001, my current research still has us referring to SICP on a regular basis, and in 2006 Kaijen Hsiao and I were the TAs for what was basically the first offering of the class that quasi-replaced it (6.01) taught by Leslie Kaelbling, Hal Abelson, and Jacob White.

I would defer to lots of people who know the story better than me, but here's my understanding of the history. When the MIT EECS intro curriculum was redesigned in the 1980s, there was a theory that an EECS education should start with four "deep dives" into the four "languages of engineering." There were four 15-unit courses, each about one of these "languages":

- 6.001: Structure and Interpretation of Computer Programs (the "procedural" language, led by Abelson and Sussman)

- 6.002: Circuits and Electronics ("structural" language)

- 6.003: Signals and Systems ("functional" language)

- 6.004: Computation Structures ("architectural" language)

These were intellectually deep classes, although there was pain in them, and they weren't universally beloved. 6.001 wasn't really about Scheme; I think a lot of the point of using Scheme (as I understood it) is that the language is so minimalist and so beautiful that even this first intro course can be about fundamental concepts of computer science without getting distracted by the language. This intro sequence lasted until the mid-2000s, when enrollment in EECS ("Course 6") declined after the dot-com crash, and (as would be expected, and I think particularly worrisome) the enrollment drop was greater among demographic groups that EECS was eager to retain. My understanding circa 2005 is that there was a view that EECS had broadened in its applications, and that beginning the curriculum with four "deep dives" was offputting to students who might not be as sure that they wanted to pursue EECS and might not be aware of all the cool places they could go with that education (e.g. to robotics, graphics, biomedical applications, genomics, computer vision, NLP, systems, databases, visualization, networking, HCI, ...).

I wasn't in the room where these decisions were made, and I bet there were multiple motivations for these changes, but I understood that was part of the thinking. As a result, the EECS curriculum was redesigned circa 2005-7 to de-emphasize the four 15-unit "deep dives" and replace them with two 12-unit survey courses, each one a survey of a bunch of cool places that EECS could go. The "6.01" course (led by Kaelbling, Abelson, and White) was about robots, control, sensing, statistics, probabilistic inference, etc., and students did projects where the robot drove around a maze (starting from an unknown position) and sensed the walls with little sonar sensors and did Bayesian inference to figure out its structure and where it was. The "6.02" course was about communication, information, compression, networking, etc., and eventually the students were supposed to each get a software radio and build a Wi-Fi-like system (the software radios proved difficult and, much later, I helped make this an acoustic modem project).

The goal of these classes (as I understood) was to expose students to a broad range of all the cool stuff that EECS could do and to let them get there sooner (e.g. two classes instead of four) -- keep in mind this was in the wake of the dot-com crash when a lot of people were telling students that if they majored in computer science, they were going to end up programming for an insurance company at a cubicle farm before their job was inevitably outsourced to a low-cost-of-living country.

6.01 used Python, but in a very different way than 6.001 "used" Scheme -- my recollection is that the programming work in 6.01 (at least circa 2006) was minimal and was only to, e.g., implement short programs that drove the robot and averaged readings from its sonar sensors and made steering decisions or inferred the robot location. It was nothing like the big programming projects in 6.001 (the OOP virtual world, the metacircular evaluator, etc.).

So I don't think it really captures it to say that MIT "switched from Scheme to Python" -- I think the MIT EECS intro sequence switched from four deep-dive classes to two survey ones, and while the first "deep dive" course (6.001) had included a lot of programming, the first of the new survey courses only had students write pretty small programs (e.g. "drive the robot and maintain equal distance between the two walls") where the simplest thing was to use a scripting language where the small amount of necessary information can be taught by example. But it's not like the students learned Python in that class.

My (less present) understanding is that >a decade after this 2006-era curricular change, the department has largely deprecated the idea of an EECS core curriculum, and MIT CS undergrads now go through something closer to a conventional CS0/CS1 sequence, similar to other CS departments around the country (https://www.eecs.mit.edu/changes-to-6-100a-b-l/). But all of that is long after the change that Sussman and Wingo are talking about here.

You don't need ATSC 3.0 to do this kind of thing! The short-term stability of the oscillators they use for commercial DTV transmission is apparently good enough that just having one local reference to compare GPS vs. each TV station's phase (and distribute that data) can produce a pretty good positioning system. Rosum was doing this back in 2005: https://www.tvtechnology.com/news/tv-signals-used-for-geopos...

I think you're both right in a sense. Bazel doesn't (in general) prevent filesystem access, e.g. to library headers in /usr/include. If those headers change (maybe because a Debian package got upgraded or whatever), Bazel won't know it has to invalidate the build cache. I think the FAQ is still technically correct because upgrading the Debian package for a random library dependency counts as "chang[ing] the toolchain" in this context. But I don't think you'd call it hermetic by default.

Check out the previous discussion at https://news.ycombinator.com/item?id=23184843 and below:

Under the hood there's a default auto-configured toolchain that finds whatever is installed locally in the system. Since it has no way of knowing what files an arbitrary "cc" might depend on, you lose hermeticity by using it.

The first edition of SICP came out in the fall of 1984 (a year after these Hofstadter columns). This fall is the 40th anniversary!

No -- as discussed upthread, clang's musttail attribute requires the target function to have the same number of arguments as the caller and for each argument to be similar to the corresponding caller argument. That's stricter than the underlying LLVM musttail marker (when targeting the tailcc/swifttailcc calling conventions) and is too restrictive to implement Wasm's tail-call feature (and probably Scheme's, etc.), at least if arguments are getting passed to functions natively.

It would be nice if the more relaxed rules of the LLVM musttail marker with tailcc could be exposed in clang (and gcc). I think that's basically what "return goto" would do.

Yes, wasm2c implements the Wasm tail-call feature with trampolines, exactly this way. (https://github.com/WebAssembly/wabt/blob/main/test/wasm2c/ta... has an example.)

Doing it with a trampoline is probably slower than if C really had tail calls. On the other hand, adding "real" tail calls to C would probably require changing the ABI (e.g. to "tailcc" or "fastcc -tailcallopt"), and I think there's some reason to think this would probably impose a penalty everywhere (https://llvm.org/docs/CodeGenerator.html#tail-call-optimizat...).

I don't think that's quite right -- I think you're thinking of 1601 S. California Ave. Faceboook had there and 1050 Page Mill, but not 1501 Page Mill afaik -- that was HP/HPE until recently and is still an office building, now leased by Tesla.

After Facebook moved out of 1601 California Ave. in 2011, it was leased to Theranos. Then it (and some of the buildings on adjacent parcels) got knocked down to turn it into a Stanford faculty housing development that opened in 2017-2019 (University Terrace). I think that's the only housing in the Stanford Research Park.

My understanding is that jitter refers to essentially stochastic variation of an ideally isochronous/periodic process or signal. You might say "the event is supposed to occur exactly every 1 second; in practice we observed jitter of +/- 50 milliseconds," referring to the RMS (1-standard-deviation estimate) of a sample of inter-event durations. Wikipedia has a nice article: https://en.wikipedia.org/wiki/Jitter

In the context of video, I think the most common use of "judder" is about the deterministic and periodic variation in timing that occurs when content of one frame rate is shown on a different-rate display. The most common situation is a "3:2 pulldown," where 24 frame-per-second film content is adapted to a 60 field-per-second or frame-per-second video signal. This is done by repeating one film frame for 3 video fields/frames (so 3/60 seconds), and then the next film frame for 2 video fields/frames, then the next one for 3, then 2, then 3, then 2, etc. (2/5 = 24/60 so it works out on average.) That repeating variation in frame duration or number of repetitions is seen as "judder." With a cinema projector or recent TV, you don't have this; the frames are shown 1/24 s apart and with an equal number of flashes each. But on an older 60 Hz TV, you'll have judder.

(I've also seen "judder" occasionally used to refer to the stuttery motion that comes from showing 24 fps content on a sample-and-hold display, like an OLED [without black-frame insertion] or a "good" LCD that just shows each frame with constant brightness for the entire 1/24 s and then almost-instantly switches to the next frame. But I don't think this is the correct usage.)

You're definitely right that Boston Light is officially in Hull, but The Graves (still a USCG-managed lighthouse, and bigger than Boston Light) is in Boston. See https://arc-gis-hub-home-arcgishub.hub.arcgis.com/datasets/m...

I met Sally Snowman a few times -- we used to visit Boston Light 1-2 times every summer on MIT's sailboat with a group of students. She was super-welcoming and shared a ton of knowledge and stories about the lighthouse and station. We really enjoyed seeing the lens, etc., and thinking we were like the MIT students in the 1890s who lived out there to try to understand how sound traveled across the sea and create a better foghorn, I think not with a ton of success.

One time we arrived at Little Brewster and I was wearing a "captain's hat" that some friends had gotten me from West Marine, and the Coast Guard auxiliarists who helped us dock gave me a hard time, Boston-style. I think they don't love it when recreational sailors wear pretend rank insignia. They were smiling about it but I didn't wear the hat on later visits!

I hope she has a great retirement and they find somebody even half as dedicated to be her successor. The only reason Boston Light still has a keeper at all (the only one left in the country) is because Ted Kennedy and John Kerry sponsored an amendment to the 1989 Coast Guard Authorization Act to the effect that "The Boston Light shall be operated on a permanently manned basis." I just went back to look at it and in Ted Kennedy's remarks he says, "Thousands of visitors a year come out in Boston Harbor to visit to Boston Light. They learn about the history of the Light from the museum exhibits at its base. They climb the historic tower, and enjoy the view of the Boston skyline and the charm of Little Brewster Island. Most important, they gain a new understanding and appreciation of the important work of the Coast Guard and the role of Boston Light in our Nation's history." The part about thousands of visitors coming out I think is sadly no longer true. :-(

The goal usually isn't for one party to take a C program and transform it into "safe" machine code. The goal is for a possible adversary to take a C program and produce an IR, and then for somebody else (maybe you) to validate that IR and produce safe machine code. Wasm is a vastly better interchange format between distrustful parties than C would be!

(There are probably even better interchange formats coming on the horizon; Zachary Yedidia has some cutting-edge work on "lightweight fault isolation" that will be presented at the upcoming ASPLOS. Earlier talk here: https://youtu.be/AM5fdd6ULF0 . But outside of the research world, it's hard to beat Wasm for this.)

Less important: I don't think going through Wasm has to be viewed as an "extra step" -- every compiler uses an IR, and if you want that IR to easily admit a "safe" lowering (especially one that enforces safety across independently compiled translation units), it will probably look at least a little like Wasm, which is quite minimal in its design. Remember that Wasm evolved from things like PNaCl which is basically LLVM IR, and RLBox/Firefox considered a bunch of other SFI techniques before wasm2c.

Well, a bunch of ways.

It's much faster to execute than adding a software bounds-check on every load. (Because the module declares its memories explicitly, it's very easy for a runtime to use a zero-cost strategy to enforce that memory loads/stores are all in-bounds.)

But Wasm's safety is more than bounds-checking memory loads/stores. E.g., Wasm indirect function calls are safe, including cross-module function calls for modules compiled separately, because there's a runtime type check (which wasm2c does very efficiently, but not zero-cost).

And, Wasm modules are provably isolated (their only access outside the module is via explicit imports). Whereas if you wanted that from "normal C code," it's a lot harder -- at some point you'll have to scan something (the source? the object file?) to enforce isolation and make sure it's not, e.g., jumping to an arbitrary address or making a random syscall. There's obviously a huge amount of good work on SFI but it's not easy to do either on "normal C code" or on arbitrary x86-64 machine code.

It takes tens or hundreds of microseconds to launch a new thread on Linux, and tens or hundreds of milliseconds (or more) to launch a new VM.

It takes tens of cycles to instantiate a Wasm module and call one of its exported functions.

There are some serious benefits to OS-mediated hardware isolation, but there are also some real benefits to the "ahead-of-time" isolation you can get from something like Wasm (e.g. via wasm2c->a C compiler->machine code, but also with more mainstream tools like wasmtime).

wasm2c (part of WABT) does this transpilation in a spec-conforming way; it passes all* the WebAssembly tests and enforces the memory-safety and determinism requirements and the rest of the spec. The memory bounds-checking itself doesn't have a runtime performance impact because it's all done with mprotect() and a segfault handler. (There are some other differences between w2c2 and wasm2c that also have to do with spec-conformance and safety; e.g., enforcing type-safety of indirect function calls. This costs <4 cycles but it's not zero.)

Re: bounds checks, the thing that consumes cycles isn't the bounds check itself, it's Wasm's requirement that OOB accesses produce a deterministic trap, even if the result of an OOB load is never observed and could be optimized out. wasm2c has to prevent the compiler from optimizing out an unobserved OOB load, and that forced liveness defeats some compiler optimizations (probably more than it needs to). But even with all that, we're talking like a <30% slowdown compared with native compilation across the SPECcpu benchmarks.

If you want to transpile arbitrary Wasm to native code in a spec-conforming way, you're probably better-off using wasm2c (which, disclosure, I work on). If you trust the Wasm module, or you're good with the isolation you get from your operating system and don't need Wasm's determinism, w2c2 seems great. Both of these are far less battle-hardened than V8 or wasmtime, especially when you include the fact that now you need an optimizing C compiler in the TCB.

---

* The Wasm testsuite repo has recently merged in the "v4" version of the exception-handling proposal, and WABT is still on "v3". But it does pass all the core tests (including tail calls) at least until GC is merged.

ObNote that in standard English it's "premises," even for a single building. Some explanation here: https://ahdictionary.com/word/search.html?q=premises

:-) The UTF-8/Unix FAQ and existing terminal emulators don't agree with you here. As you say, there's no spec for this, but here's what Kuhn's FAQ says (https://www.cl.cam.ac.uk/~mgk25/unicode.html#term):

"UTF-8 still allows you to use C1 control characters such as CSI, even though UTF-8 also uses bytes in the range 0x80-0x9F. It is important to understand that a terminal emulator in UTF-8 mode must apply the UTF-8 decoder to the incoming byte stream before interpreting any control characters. C1 characters are UTF-8 decoded just like any other character above U+007F."

The existing ANSI terminal emulators that support UTF-8 input and C1 controls seem to agree on this (VTE, GNU screen, Mosh). xterm, urxvt, tmux, PuTTY, and st don't seem to support C1 controls in UTF-8 mode. So I don't think poking holes in the UTF-8 decoder is necessary, especially since allowing C1 in UTF-8 mode is rare anyway.

FWIW, I wouldn't try to parse escape sequences directly from the input bytestream -- it's easy to end up with annoying edge cases. :-/ In my experience you'll thank yourself if you can separate the logic into something like:

- First step (for a UTF-8-input terminal) is interpreting the input bytestream as UTF-8 and "lexing" into a stream of Unicode Scalar Values (https://www.unicode.org/versions/Unicode15.1.0/ch03.pdf#P.12... ; https://github.com/mobile-shell/mosh/blob/master/src/termina...).

- Second step is "parsing" the scalar values by running them through the DEC parser/state machine. This is independent of the escape sequences (https://vt100.net/emu/dec_ansi_parser ; https://github.com/mobile-shell/mosh/blob/master/src/termina...).

- And then the third step is for the terminal to execute the dispatch/execute/etc. actions coming from the parser, which is where the escape sequences and control chars get implemented (https://www.vt100.net/docs/vt220-rm/ ; https://invisible-island.net/xterm/ctlseqs/ctlseqs.html ; https://github.com/mobile-shell/mosh/blob/master/src/termina...).

Without this separation, it's easier to end up with bugs where, e.g., a UTF-8 sequence or an ANSI escape sequence is treated differently if it's split between read() calls (https://bugs.chromium.org/p/chromium/issues/detail?id=212702), or invalid input isn't correctly recovered-from, etc.

No -- in 2019 Google Ad Manager announced it was moving to a first-price auction (https://blog.google/products/admanager/simplifying-programma...) and AdSense followed in 2021 (https://support.google.com/adsense/answer/10858748?hl=en). (Edit: With regard to Google Ads for Search, they no longer seem to commit to any particular algorithm for deciding what price gets paid.)

There are some lawsuits that allege that Google was effectively cheating before then, by sort of manufacturing a shill bidder, with privileged access to everybody's bids, that turned it into something closer to a first-price auction (https://www.wired.com/story/google-antitrust-ad-market-lawsu...). The quotes from within Google look pretty bad, e.g. one Googler allegedly wrote: "Doesn’t that undermine the whole idea of second price auctions? I.e., the assurance that you can bid the maximum you’re willing to pay with no negative consequence. But if the publisher manufactures a floor based on your bid to get you to pay more than the second price, this principle gets violated. It’ll transform the system into a 1st price auction where the bidder has a strong incentive to bid LESS than he’s willing to pay. (Only just enough to win.) I don’t think that’s desirable for either side in the long term."

Google... disputes this (https://blog.google/outreach-initiatives/public-policy/ag-pa...). I guess we'll see.

For clarity, you don't really need a "browser-grade sandbox" for this -- the wasm2c route that Firefox/RLBox are using is quite lightweight. The only runtime support necessary is basically malloc/free + a signal handler to recover from OOB accesses (and even the signal handler is optional if you can tolerate a runtime slowdown). It's usually pretty easy to compile and link wasm2c's output with an executable that can speak the C ABI.

(I've contributed to wasm2c and think it's a cool tool.)

Not so -- 1080p24 and 1080p30 sequences (and the 1000/1001-rate versions) were part of the original A/53 specification in 1995. This is for H.262 video (MPEG-2 part 2). It's also in the 2007 revision (see A/53:2007 part 4, table 6.1.2 [1]). In practice, what broadcasters really do is send a sequence labeled 1080i30 for everything, but during the 24P content, they send 24 progressive-scan frame pictures per second, with picture flags that instruct the decoder how to perform the 3:2 pulldown to manufacture 60 fields per second at the receiver. This kind of "1080p24" is very common and they've been doing it since the 90s or early 2000s. The same basic technique is used on NTSC DVDs.

([1] https://prdatsc.wpenginepowered.com/wp-content/uploads/2021/.... Pedantic note: What the FCC adopted is slightly more generous than the ATSC spec; they excluded this table, both pre- and post-2007. So technically speaking, anything "Main Profile @ High Level" is allowed on the U.S. airwaves, but it doesn't matter in practice.)

Just to be pedantic, 1080p24 (and 1080p30, and the 1000/1001-rate versions) are already allowed by the existing A/53 spec and have been since 1995. The big (1080-line) broadcasters usually transmit their film-style programming as "effectively" 1080p24, in the sense that they're sending 24 or 24000/1001 progressive-scan coded pictures per second, but with flags that ask the decoder to perform a 3:2 pulldown to output 60 fields per second so it fits seamlessly within a 1080i30 sequence. (They could be sending "true" 1080p24, but then it would probably create a glitch when they transition to 60 fps content and back.)

But anyway: 1080p itself is not a new feature of ATSC 3.0. 1080p60 or 1080p120, sure.

FWIW, the arithmetic in that example also has a glitch. For the "Mobile" "Control" case, 100/3000 is about 3% rather than 10%.