Of course there are some systems where correctness is vital, and for those I'd like a precise spec and proof of correctness. But I think there's a huge bulk of code where formal specification impedes what should be a process of learning and adapting.

Here's a recent ShowHN post (a map view for OneDrive photos), which documents all the LLM prompting that went into it:

https://news.ycombinator.com/item?id=44584335

Parent: "5% chance of looking as good as it did, if it were truly no better than the alternative." This accepts the premise that the product quality is a fact, and only uses probability to describe the (noisy / probabilistic) measurements, i.e. "5% chance of looking as good".

Parent is right to pick up on this, if we're talking about a single product (or, in medicine, if we're talking about a single study evaluating a new treatment). But if we're talking about a workflow for evaluating many products, and we're prepared to consider a probability model that says some products are better than the alternative and others aren't, then the author's version is reasonable.

(Though if you have a reference for why empirical Bayes does give theoretical guarantees, I'll be happy to change my mind!)

A Bayesian could try the same thing: try out several priors, and pick the one that performs best in validation. But if you pick your prior based on the data, then the classic theory about “principled quantification of uncertainty” doesn’t apply any more. So you’re left using a computationally unwieldy procedure that doesn’t offer theoretical guarantees.

[0] https://news.ycombinator.com/item?id=38965003

[1] https://xkcd.com/1168/

[0] https://en.wikipedia.org/wiki/%C3%9F

Pyodide includes manyuseful Python libraries including numpy, pandas, and matplotlib.

Why isn't it commonplace? I think that touchscreen laptops are still too much a minority, and keyboard + mouse + monitor are too entrenched, for anyone to seriously attempt it again for a while. (A shame -- I'm one of the few who really liked the Windows 8 Metro interface.) I think that phones are too small for it to really work well. I don't know why it's not more popular on tablets.

Also, frequentism / Bayesianism is orthogonal to causal / correlational interpretations.

I've asked students to share their full dialog, both prompts and replies, so the whole class gets to see; and I'll invite one or two to talk through their attempts. This is all just a trick to make students engage with "how do you you spot bugs in a proof?", hopefully more than they would from just reading CLRS! Often, students engage well when they're hearing the material from other students.

After we go through Breadth First Search, there's a practical assignment where students are asked to modify the algorithm to return _all_ shortest paths. Then I ask ChatGPT for its solution, and students try to spot its mistakes.

Later, after going through the proof of correctness of Dijkstra's algorithm, I ask ChatGPT for a proof of correctness of its all-shortest-paths algorithm, and again students try to spot what's wrong in the proof. I want students to learn to tell the difference between a bullshit proof and a real proof; in the past I've given them bullshit proofs from real students in exams, but ChatGPT makes the point more nicely.

Finally, students are asked to figure out prompts that will make ChatGPT give a correct algorithm and proof. I haven't managed this myself! I'm looking forwards to seeing what students manage.

Here's a link to lecture notes, including the ChatGPT dialog: https://www.cl.cam.ac.uk/teaching/2223/Algorithm2/alg2-full....