One pattern I have observed and guilty of myself is that simple hybrid search patterns work poorly on single-word intent queries. It is better to do pure lexical search for certain queries and then fallback to semantic or hybrid.
I've settled into a habit of asking codex to write down summary of key decisions in a ledger as I end a unit of work. It keeps iterating natural but maintains a system of record on decisions in the same repo. The "ledger" is the new code.
I believe these are called Architectural Decision Records. Matt Pocock's skills [0] make use of them. They're one of the more useful things I've gotten out them.
If anyone is looking to retrofit to an existing pipeline, I use similar ideas to compress vectors for job search, getting roughly 8x compression with about a 3.5% drop in quality. My experiment: https://corvi.careers/blog/vector-search-embedding-compressi...
Perhaps model size and reasoning length trade off to some extent, similar to CPU vs. RAM. A smaller model with a longer reasoning trace has more intermediate structure to latch onto and build on.
Suppose I write a distributed algorithm in Rust. To verify it, I might describe the algorithm again in TLA+, model-check that specification, and prove that it satisfies the properties I care about.
Now I have two artifacts:
TLA+ specification --> proved
Rust implementation --> runtime
But the proof establishes something like:
TLA_Spec => Safety
What I actually need is:
Rust_Program => Safety
I believe this is called model-code gap and there are ways to address it but I haven't found an easy-to-follow approach.
I last touched formal verification methods 20 years ago. Back then, Coq had the capacity to automatically transform your proof into OCaml. I would have expected that this would have only gotten better with time.
I really wish one of these projects overcomes its academic origins and becomes a software development tool. Kani is closest to that pragmatism, but correspondingly its theory side is not quite as powerful -- though it's been getting new features that make real code easier to deal with, earlier when I played with it it could only reason about very simple functions. Flux also looked surprisingly approachable, but I haven't used it in anger yet.
There's hope that Rust will include language-level conventions for expressing contracts that all these tools can then take advantage of, because e.g. a `verus! {}` macro wrapping everything was never gonna be a viable way forward, and hopefully this will also gives us a syntax that looks like programming not math (I'm looking at you, Creusot): https://github.com/rust-lang/rust/issues/128044
Not just that, I've been seeing a huge effort in the Ada community to leverage LLMs to convert a lot of libraries into formally verified SPARK code. One of the biggest issues I see with vibe coded stuff is that it's difficult to review and difficult to prove that it's doing what you think it's doing, but with a strongly type language like Ada and formal verification with SPARK, LLM output is easy to read and easy to prove.
I think the reality is that it has to be baked into the language. Here's my real attempt at that - if you model the system in the language, the compiler can reason about the distributed fleet: https://hale-lang.org/proof/
I think the gap is real and for it to be resolved, the spec language needs to be elevated to a source of truth and possibly do some degree of codegen, which is currently not well realized with Lean
The analogy I'd make is to the idea of "type driven development" that buf/protoc represent, where one defines their types and schema in proto and then types for specific languages are generated from that
The limitations there however is that proto is not a programming language and inflexible/inexpressive whereas Lean is one of the most expressive languages to date
LLMs are pretty good at this. Not perfect by any means as the model is just a model after all - always wrong, sometimes useful - but the act of writing a TLA+ model helps the frontier LLMs to write correct executable code. It also works the other way around - given code, it can build a model in TLA+ and find latent bugs which it'll likely miss otherwise. (https://github.com/specula-org/Specula)
As I remember it, he was formalising compilation by connecting the semantics of the higher level to the lower level one inside the proof assistant, so that proofs would carry through.
In my opinion, it's not very different than writing an implementation of quicksort by looking at pseudocode in an algorithms book. You still need to write unit/property tests for your implementation if you want to verify it to be correct.
Any time you code up an externally specified algorithm, the onus is still on you to verify your implementation, even if the correctness of the algorithm is already verified.
Something like TLA is to prove the design of an algorithm is what you intended.
Proving a specific implementation in a specific language is really the domain of that language or tools targeting that language.
In digital design for example, SystemVerilog has a whole sub-language for specifying formal properties that can be proved in simulation or with tools that prove the properties mathematically.
Good observation. This is an employer hiring demand index, not a measure of overall technology usage and my coverage is strongest among larger employers and organizations publishing through tracked ATS/job posting sources, so that could explain it.
It tracks explicit mentions of ~ 181 languages, technologies, vendors, etc as seen in job postings. The motivation was that GitHub activity and developer surveys describe what people use or enjoy, but not necessarily what employers are requesting.
The annoying part is a large percentage of misbehaving bots (not obeying robots.txt for example) are via end user proxies across the world. However most of these aren't doing full-browser loop, so if you are behind cloudflare, you can do non-interactive challenge and that can help quite a bit.
It's tough to trust job openings. It is a fact that some number of job postings are ghost jobs that don't exist. Either they're scams from impersonators or the companies are trying to keep a good public face, but many openings sit for MONTHS which just does not line up with the anecdotal evidence of people going 6-12 months without an interview much less an offer
Some of these offers may be part of visa or green card processes. Some require a labor market test in the form of a job ad and recorded response to it. If a suitable candidate applies, the visa/immigration process fails. Still, most companies don't intend to actually hire in this case as far as I understand it.
> but many openings sit for MONTHS which just does not line up with the anecdotal evidence of people going 6-12 months without an interview much less an offer
Neither of these things are evidence of “ghost jobs”.
When I was doing a lot of hiring it would often take months to find qualified candidates for basic roles. I would get 100s of applicants per month but only about 20% of the resumes I received were even close to qualified. I’d try to schedule intro and screening calls with the qualified ones who would actually respond, but you wouldn’t believe how many applicants would have unreliable communication skills. Some times I wouldn’t get a response from someone for weeks or more, but many just don’t respond to contact after applying to your company. If we’re using the lingo I think a lot are “ghost candidates”.
There’s further fallout through the interview pipelines as you discover how many people have lied on their resume or otherwise aren’t qualified. That self-styled C++ expert who can’t give an example of RAII or the self-proclaimed TypeScript expert who doesn’t know anything outside of vanilla JavaScript. It’s weird.
Then there are negotiations. Some candidates want to collect offers from multiple companies and will ask for delays in hiring so they can continue interviewing and getting other offers. It can take weeks for some candidates to accept or decline your offer. If they decline you have to go to the next candidate, which can take more weeks, and then on to the next. If there’s relocation involved it takes longer to decide and get it done.
Then some times we’re hiring multiple people for a row, so we leave the listing up and open to continue hiring. This really angers the “ghost jobs” people because they assume 1 listing == 1 hire, as if the company needs to close the listing and then copy/paste to a new URL for the next hire.
So job openings that exist for “MONTHS” are not evidence of ghost jobs.
The people going 12 months without an interview are almost always doing something wrong. You wouldn’t believe how inexcusably bad many of the resumes out there can be. Some people are hung up on applying only to jobs they aren’t qualified for and then wonder why they’re not getting interviews.
maybe, but ghost listings have to be posted at some point, and who knows how long the companies want to let them go (and sometimes they expire and someone needs to refresh them)
they're not all ghost jobs, and there is probably a base level of noise there you can ignore, but the variability doesn't mean the data is great and perfect
Yup, and my data only captures a part of professional job market which itself is small part of labor market. I'd use this as additional data point to other sources to correlate etc. However, the experiment is mostly to test my own thesis that unless there is a major event like covid, these trends are really hard to spot.
