233 karma · joined December 19, 2022
> If the algorithm terminates with b = 1, what must have been true at the start?
For anyone that wasn't clear, "b" isn't the number of beans in general, it's specifically the the number of black beans. Introducing a variable before defining what it is can be a bit confusing, hope this comment helps others.
There are two main differences between our system and the one in the post:
- In our scheduler, the actual cron (aka recurrence rule) is stored along with the task information. That is, you specify a period (like "every 5 minutes" or "every second Tuesday at 2am") and the task will run according that schedule. We try to support most of the RRule specification. [1] If you want a task to just run one time in the future, you can totally do that too, but that's not our most common use case internally.
- Our scheduler doesn't perform a wide variety of tasks. To maximize flexibility and system throughput, it does just one thing: when a schedule is "due", it puts a message onto a queue. (Internally we have two queueing systems it interops with -- an older one built on top of Redis, and a newer one built on PG + S3). Other team consume from those queues and do real work (sending emails, generating reports, etc). The queueing systems offer a number of delivery options (delayed messages, TTLs, retries, dead-letter queues) so the scheduling system doesn't have to handle it.
Ironically, because supporting a high throughput of scheduled jobs has been our biggest priority, visibility into individual task executions is a bit limited in our system today. For example, our API doesn't expose data about when a schedule last ran, but it's something on our longer term roadmap.
[1] https://icalendar.org/iCalendar-RFC-5545/3-8-5-3-recurrence-...
- The sharp contrast between the '90s "Jeffersonian", hacker-libertarian spirit and today's more "Hamiltonian", state-capacity mindset, and how they're tied to the geopolitical and technical shifts that nurtured each era.
- The clear taxonomy of the new "tribes" (EA, abundance, American dynamism, New Right, tech ethicists, network-staters) and the axes they vary across -- human nature, progress vs preservation, role of the state. Nadia did a similar breakdown of climate activist tribes in "Mapping out the tribes of climate" a few years ago that I thought was interesting as well.
- There are some data nuggets that upend cliches, e.g. nine VCs controlling ~50% of 2024 fundraising, and tech elites being less anti-government than either party’s base.
- The insight that valley thinking now shapes national politics (e.g. J.D. Vance), showing tech culture's reach beyond product launches.
To me this raises the question of whether this is a growing trend, or whether it's simply that languages staying closed source tends to be a death sentence for them in the long term.
I've never been a [traditional] artist, but I reckon that those working in the arts, and even areas of the programming world where experimentation is more fundamental (indie game development, perhaps?), would intuit the importance of discovery coding.
Even when you're writing code for hairy business problems with huge numbers of constraints and edge cases, it's entirely possible to support programmers that prefer discovery coding. The key is fast iteration loops. The ability to run the entire application, and all of its dependencies, locally on your own machine. In my opinion, that's the biggest line in the sand. Once your program has to be deployed to a testing environment in order to be tested, it becomes an order of magnitude harder to use a debugger, or intercept network traffic, or inspect profilers, or do test driven development. It's like sketching someone with a pencil and eraser, but there are 5-10 second delays between when you remove your pencil and when the line appears.
Unfortunately, it seems like many big tech companies, even that would seem to use very modern development tooling otherwise, still tend to make local development a second class citizen. And so, discovery coders are second class citizens as well.
I had a similar idea a few months ago about whether it's possible to achieve some form of comptime with TypeScript. I didn't get too far unfortunately, but I think the implementation would need to interact with the TypeScript compiler API in some way.
sig FSObject { parent: lone Dir }
sig Dir extends FSObject { contents: set FSObject }
sig File extends FSObject { }
// A directory is the parent of its contents
fact { all d: Dir, o: d.contents | o.parent = d }
// All file system objects are either files or directories
fact { File + Dir = FSObject }
// There exists a root
one sig Root extends Dir { } { no parent }
// File system is connected
fact { FSObject in Root.*contents }
// Every fs object is in at most one directory
assert oneLocation { all o: FSObject | lone d: Dir | o in d.contents }
I initially thought these model checking languages were purely academic in nature. But then a curious problem came up when I was working at AWS where folks were complaining that IAM policies generated by our library were sometimes growing to be too large in size (usually the limit was a few KB) - often due to redundant statements.To solve this, a coworker implemented some code for merging IAM policies -- though the merging processe wasn't trivial because IAM policies can have both "Resources" and "NotResources", "Actions" and "NotActions", "Principals" and "NotPrincipals" etc. So to prove the algorithm was correct, he wrote up a short Alloy specification[1] (roughly mapping to the library code) that proved if two policy statements were merged, it wouldn't change the security posture. As a new engineer to the team, I'll just say that it blew my mind that this was possible -- actually using proofs to achieve goals in industry.
Needless to say, I'm curious to dive into Quint's differences and what kinds of models/specifications it excels with.
[1] https://github.com/aws/aws-cdk/blob/main/packages/aws-cdk-li...
NOUN 147 slob, Ellie, silo, bile, sell, Gil, belles, highs, Bessie, losses, giggles, Liz, hobo, Leslie, Bob, lies, bellies, soil, Hess, hells, Isis, Gog, Hiss, boogie, holes, bliss, oils, gel, leg, lobes, globes, Gill, Leigh, geese, bogies, bilge, Lizzie, Leo, boil, legs, shoe, shells, Ozzie, giggle, ooze, size, eel, high, bill, gob, hole, hog, soles, libel, Hill, bee, shills, ills, Lois, glee, Bess, lobe, gig, Beebe, sizes, Gogol, sloe, hiss, Ellis, Sol, boos, Ohio, bees, HBO, bobbles, ill, lie, sobs, booze, bibles, Gibbs, hobbies, sighs, shell, isle, bib, Hegel, hills, Zoe, Eloise, Giles, sill, Elsie, Bill, bells, loss, egg, eggshell, bills, hoses, Shiloh, siege, Bible, solos, sigh, Hillel, logs, hose, lobbies, hill, log, hob, bell, shoes, Lee, gloss, heels, Hobbes, bosses, soils, solo, Oslo, hoes, goose, oil, Bell, blob, goggles, Eli, sole, ego, silos, hogs, lilies, Billie, gibes, ell, hell, shill, globe, oblige, loose, eggs, gibe, boss, heel, Bobbie
VERB 34 sells, loses, Lie, boil, sell, ebb, lob, seize, solo, begs, see, ebbs, sizzle, beg, lie, besiege, ooze, size, goes, hole, lies, hobble, bog, obsesses, soil, boils, loose, bless, solos, sigh, gobbles, shies, lose, sees
ADJ 9 sole, loose, ill, high, less, glib, big, beige, eligible
ADV 5 loose, ill, less, high, else
PRT 4 gosh, hello, see, hell
X 3 his, Les, les
DET 1 his
PRON 2 his, she
Personally I feel like debates around serverless would be more interesting and productive if the industry had a better understanding of what kinds of applications actually benefit from these kinds of architectures (I/O bound workloads? Compute-bound workloads? Or is it just best as a stepping stone for prototypes and for teams without ops experience?)
let bucket = new cloud.Bucket();
let api = new cloud.Api();
// api.get is a preflight method - it generates cloud infrastructure
api.post("/hello", inflight (req) => {
// bucket.put is an inflight method - it performs data plane operations, at "runtime"
bucket.put("data.txt", req.body ?? "empty");
});
Importantly, if you try calling bucket.put() outside of one of these "inflight" scopes or try calling api.get() inside one of these "inflight" scopes, you'll get compilation errors - not runtime errors.Could this style of API be achieved in an existing language? I think it's an open ended question - I'm not sure. But I reckon it gets into complex framework territory (or may require injecting modifications into existing compilers, which presents other challenges). But I'd love to see more exploration into this direction.
Your observation is partially correct. The language does make a distinction when you're defining new functions: you must use the "inflight" keyword annotation to define an inflight function, and most un-annotated functions are assumed to be "preflight". (The top-level scope of every Wing program has a preflight phase).
But at _call sites_ no distinction is made. We don't have have a different calling convention between calling preflight/inflight functions because the compiler uses type checking to enforce that inflight functions can only be called in inflight scopes, and preflight functions can only be called in preflight scopes. Scopes are lexical, meaning you can automatically assume when you see `inflight () => { ... }` or `inflight foo() { ... }` that all code inside that block is executed inflight, i.e. at runtime.
The neat thing here is if you're writing code to access a method on a class (typing `obj.`), your IDE's auto-completion will only show you the methods available to you based on the scope you're in. There's a short 10 second clip showing this here: https://twitter.com/rybickic/status/1720168675641102803
We've prioritized LSP support while designing the compiler to help out with this.
In this case, the main thing that was "fast" was that I didn't have to rewrite a nontrivial string formatting library in a new language (I literally couldn't find any other JavaScript libraries that had this kind of error-formatting functionality, so that would have been my only other option). :-)
> New languages == zero ecosystem—no third-party libraries, community discussion (e.g. StackOverflow), real-world repositories, etc.
Bootstrapping a language ecosystem is a challenge we know we needed to face from day 1. To avoid starting from scratch, we're designing the language to compile to JavaScript as an intermediate format so that we can add native syntaxes for users to import JavaScript/TypeScript libraries and leverage that existing ecosystem. Our type systems are not the same, but we're trying to make sure users can still be productive and that things "make sense" out of the box, in case you want to import libraries like axios, express, etc.
We are also designing it to interoperate with the existing ecosystem of "CDK" libraries (https://constructs.dev/) that tens of thousands of developers have already been using to write abstractions for cloud resources based on Terraform, CloudFormation, and Kubernetes.