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.
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
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).
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)
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.
> 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.
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.
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.)
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.
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.
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.