IMPORTANT: Do NOT write multi-line Python as inline python3 -c — the terminal garbles it. Always write to a file first, then run.
Run these in order. Set CONVO first:
CONVO=~/.openhands/conversations/CONVERSATION_ID
1 — Input: WebAssembly 3.0 SpecTec sources
specification/wasm-3.0/ (34 files, fed to SpecTec in numeric order)
File Covers
0.1-aux.vars.spectec Auxiliary variables
0.2-aux.num.spectec Numeric auxiliaries
0.3-aux.seq.spectec Sequence auxiliaries
1.0-syntax.profiles.spectec Profiles
1.1-syntax.values.spectec Values
| # Paste this into D2 Playground: https://play.d2lang.com | |
| direction: right | |
| classes: { | |
| outcome: { | |
| style: { | |
| shadow: true | |
| } | |
| } |
Planguage (Planning Language), developed by Tom Gilb, is a structured, keyword-driven notation designed to define project requirements, quality attributes, and goals precisely. It eliminates ambiguity in nonfunctional requirements by defining metrics, stakeholders, and targets for, example:
Tag: Unique ID (e.g., Performance).
Meter: How to measure (e.g., "Time for report").
Target: The desired level.
It is a key part of Competitive Engineering and Evo (Evolutionary) project management.
| // https://strudel.cc/workshop/getting-started | |
| // Made by Ray Myers for the Year of DSLs on "Craft vs Cruft" YouTube channel. | |
| // Apologies to the Beastie Boys. | |
| setcpm(110/4) | |
| $: note(`< | |
| [ -!6 c2 d2@2 -!7 ] | |
| [ -!4 d2 c2 a1 d1@2 -!7 ] |
Over the past year coding agents have seen massive adoption and become flagship offerings from AI leaders like Anthropic, OpenAI, and Google. Watching these agents work can feel like magic. To fully explore their potential we need to demystify them. If you're considering contributing to an Open Source agent or even creating one of your own, this should get you off to the races!
The most common style of coding agent today is a chat loop between a user and an LLM that can perform useful software development tasks. To achieve that, there are just 3 tricks to understand beyond the LLM itself.
| # LinkedIn Post | |
| # https://www.linkedin.com/posts/cadrlife_let-me-translate-the-o3-coding-benchmark-activity-7277038051590029313-yJlR?utm_source=share&utm_medium=member_desktop | |
| # Slides using the minimalist tool Sent | |
| # https://tools.suckless.org/sent/ | |
| SWE-bench | |
| SWE-bench measures AI coding agents | |
| on realistic tasks from GitHub |
| plugins { | |
| java | |
| application | |
| } | |
| group = "org.raymyers" | |
| version = "1.0-SNAPSHOT" | |
| repositories { | |
| mavenCentral() |
This is an example of hybrid use of mechanized proofs with prose in a way that favors human readers.
It's a formalization and response to the central argument in The Futurlang vs. Natural Language Debate: Should Emotion Be Eradicated From Speech?. The argument was modeled using First-Order Logic in the Z3 prover.
There can be a thing.