| # 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.
| // From this repo: | |
| // https://github.com/NoelFB/Celeste/blob/master/Source/Player/Player.cs | |
| // Linked in this thread: | |
| // https://community.revolutionarygamesstudio.com/t/bad-code-examples/106 | |
| Sprite.OnLastFrame = (anim) => | |
| { | |
| if (Scene != null && !Dead && Sprite.CurrentAnimationID == "idle" && !level.InCutscene && idleTimer > 3f) | |
| { | |
| if (Calc.Random.Chance(0.2f)) |
| LetNonRec( | |
| Def { | |
| loc_pattern: @0-5 Identifier( | |
| `Test.birds`, | |
| ), | |
| loc_expr: @8-9 Num( | |
| 63, | |
| "3", | |
| I128( | |
| [ |
| import infomap | |
| import littletable | |
| import itertools | |
| import json | |
| from sentence_transformers import SentenceTransformer, util | |
| # def simularity(functions): |
| You are an expert in software engineering including maintainability and refactoring. | |
| You have studied under Marianne Belloti, Martin Fowler, and Llewellyn Falco. | |
| For every block of source code you are given, suggest several opportunities for renames. | |
| Suggestions should help make the code more clear and honest, without being more verbose than needed. | |
| Only show suggestions, never the updated code. | |
| Keep responses brief. | |
| # Behavior | |
| You are made to receive code. Every time you receive code, print only your Hot Keys! When a hot key is pressed, take only that action. |
This is a tounge-in-cheek illustration of formal logic used refute the claim that high performers are never laid off, using that claim itself (made by an executive) as evidence that judgements are sometimes made without context.
In reality, there is no need to prove such an obvious point because by definition layoffs are not "for cause" terminations, the company has no legal responsibility to justify them as related to the impacted individuals.
The proof proceeds by first assuming P1 and showing that it leads to contradiction.
| #!/usr/bin/env python | |
| import sys, os, re | |
| from subprocess import check_output | |
| # Collect the parameters | |
| commit_msg_filepath = sys.argv[1] | |
| allowed_prefixes = ( | |
| 'f - ', 'F - ', 'F!! ', 'F**', |
| FROM 43a3a253 | |
| ENV DEFAULT_FILE=main.c | |
| ENV UNTANGLER_DEFAULT_FILE=main.c | |
| ENV JAVA_HOME=/Library/Java/JavaVirtualMachines/graalvm-jdk-20.0.2+9.1/Contents/Home/ | |
| ENV PATH="$PATH:/Users/rmyers/dev/untangler/build/install/untangler/bin" | |
| ## Aliases | |
| RECIPE move_includes_to_top \ | |
| grep "^#include" $UNTANGLER_DEFAULT_FILE > a.tmp && \ |