wcrichton

This is right -- the analysis here uses aspects of Rust which don't exist in other languages. Specifically, transitive mutability markers (&T vs. &mut T) and lifetime-based alias-analysis.

I am the main author of the tool. Vytautas has helped me get the Rust compiler integration set up :-)

The closer relation would be to Prusti [1] which is Vytautas' project on verifying Rust codebases. We use the same IR emitted by the Rust compiler.

[1] https://github.com/viperproject/prusti-dev

I didn't know about #[repr(transparent)], I will add that to the blog post. Thank you!

Hi, author of the code here. Why do I use mem::transmute? To highlight the fact that when using typestate, it's useful to understand operations that change the the value of an object as distinct from those that change the type of an object. It's also a matter of efficiency -- you don't have to generate a new struct every time you change state.

You can avoid the overhead without transmute, but it's still unsafe and not easily explained: https://github.com/Munksgaard/session-types/commit/3a310d205...

You should read the paper! http://penrose.ink/media/Penrose_SIGGRAPH2020.pdf

They include:

* Vector spaces

* Function diagrams

* Geometric illustrations

* Polygonal meshes

* Ray tracing diagrams

The linked article is pretty much fluff, but the SIGGRAPH paper has the real content.

Another great space of exercises in this vein are in-place operations on binary trees.

Specifically, rebalancing [1] proved particularly tricky for my students. I think it's a good litmus test for whether you understand ownership, borrowing, and algebraic data types.

[1] http://cs242.stanford.edu/f19/assignments/assign6/#22-bst-in...

You may be interested in Penrose (https://penrose.ink) which generates graphics of math figures from equation. I don’t know if they have as much in the way of a constraint language, but it’s certainly in a similar vein of work, and I know they use some force directed layout.

Yes, the content is on the course website: http://cs242.stanford.edu/f18/

The only prerequisites are basic discrete math (first-order logic, sets, etc.) and computer systems (C, memory management, threading) knowledge.

Thanks for the kind words!

Hi, author of the paper here, happy to answer any questions.

Having written a handful of probabilistic programs, I don’t think there’s no modularity at all. You can still abstract a complex stochastic process behind a function. I think it’s more that certain tasks are necessarily antimodular, eg doing conditional inference can introduce unexpected dependencies between modules, see d-separation [0].

[0] https://www.andrew.cmu.edu/user/scheines/tutor/d-sep.html

I’m definitely not advocating for an automated way of building these models, for the reasons you point out. Instead, I’m saying more that probabilistic models are not taught in a way that we can easily map our knowledge structures onto them, so I’m advocating for more explicit guidance in that process.

I taught this concept in my course on Programming Languages at Stanford. If you’d like a more pedagogic introduction to both session types and their implementation, check out the course notes: http://cs242.stanford.edu/f18/lectures/07-2-session-types.ht...

Does this permit Bayesian inference? e.g. looks like graphical probabilistic programming (hooking up various distributions and performing inference), except the key missing component is the ability to observe values for any given distribution beyond the prior.

For those who want to learn more, I wrote an extended, accessible introduction to session types (predicated on a little knowledge about PL metalanguage syntax, e.g. BNF grammar) here: http://cs242.stanford.edu/lectures/07-2-session-types.html

It also includes a walkthrough of a session types implementation in Rust.

Typed literal macros [0] are a principled way of integrating these kinds of mini-languages into a bigger general-purpose language.

[0] https://github.com/cyrus-/relit

Lua is a big reason why I'm interested in both systems and PL today. I started using Lua to build game mods in high school, and I was struck by how simple it was compared with Java, or even Python that I had tried learning earlier. The all-encompassing "everything is a table" paradigm really sparked my interest in the design of systems of computation, and how a broad range of programing patterns could be expressed with a few primitives.

Some specific resources for the interested:

- Cognitive Dimensions of Notations (Green 1989) http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.128...

- Programmers Are Users Too: Human-Centered Methods for Improving Programming Tools (Myers et al. 2016) http://faculty.washington.edu/ajko/papers/Myers2016Programme...

- Programmer Interrupted (Parnin 2013) http://blog.ninlabs.com/2013/01/programmer-interrupted/

- Empirical analysis of programming language adoption (Meyerovich and Rabkin 2013) https://dl.acm.org/citation.cfm?id=2509515

- Learnable Programming (Victor 2012) http://worrydream.com/LearnableProgramming/

- Usability of Programming Languages working group at CHI'16 https://docs.google.com/document/d/1-GUt5oVPpi7rlObbU1WbA5V1...

I would call that Resistance (or Avalon, Mafia, etc.). A social/trust/betrayal-oriented party game that's playable in less than an hour.

Except, WebAssembly isn't even close to Javascript. They're completely different languages. WebAssembly is closer to C than to Javascript.

Strongly recommend Types and Programming Languages [1]. I think it's the most useful + accessible book on type theory out there.

[1] https://www.amazon.com/Types-Programming-Languages-MIT-Press...

For reference, this was a course project done in my class at Stanford (CS 242: Programming Languages) last fall, not a peer-reviewed publication. Overall a great project. The title is a bit general, but the goal was to identify what resources people found most useful when learning Rust and why. My favorite bit:

> Participant behavior indicates that they found the in-line Rust Enhanced compiler errors that showed upon saving to be quite useful. Participants were not told about this feature, and only discovered it, on average, 1058 seconds (17 minutes, 38 seconds) into the task. However, after finding the Rust Enhanced compiler error feature, participants began saving every 30.6 seconds, on average, with an average of 24.8 total saves per person.

Ah, my mistake. Clarified the wording, thanks.

The phrase "most engineering PhD's are bogus" is astoundingly ignorant of the excellent work that goes on in the systems community (assuming by "engineering" you're referring to application-oriented CS research?). "Building prototypes that aren't quite useful but not quite that novel" is bad systems research, not all systems research.

Part of what this reveals is the intimate relationship between querying and labeling. A query (in the SQL sense) is the human attempting to express a domain concept through a program. Here the queries have an imperative flavor (being written in Python). From the article for example, identifying causal relationships in text by searching for “due to” is a domain concept encoded as a weak heuristic.

This suggests that our query tools need to be more deeply integrated into human-in-the-loop machine learning workflows. For example, in my use case of analyzing TV news videos, let’s say I want to identify a panel of guests. I’ll come up with a query like “3 to 5 people on screen, whose pose suggests they are sitting, and they’re looking at each other.” While this query isn’t a perfect filter (precision nor recall), it will likely find a few positive examples. Then I can query “show me more scenes like this one,” and slowly build up a training set from my queries. Then I train a classifier, and inspect its results. Rinse and repeat.

Edit: also, I’m sure there’s a billion startups that do some variant of this for some domain, but I think we really need a better open source ecosystem around visualization and labeling of data for this workflow to be truly accessible in most domains.

It stops at the product, no? It seems more acceptable to target advertisements for toys than housing.

Note that if you use open source models, it’s orders of magnitude cheaper. In my own tests, an off the shelf face DNN-based face detector [1] ran at 20 FPS on a 16 vCPU machine (Google Cloud). With our hand-rolled distributed execution engine [2], we processed around 40 million images for about $2000, which is 14x cheaper than the cheapest figure cited in OP. I don’t know the accuracy difference, but it sounds like OP will cover this in the next post.

[1] https://github.com/davidsandberg/facenet/tree/master/src/ali...

[2] https://github.com/scanner-research/scanner

Can anyone in robotics/drones speak as to how far away we are from Slaughterbots? [1]

[1] https://m.youtube.com/watch?v=HipTO_7mUOw&vl=en