Hey everyone!

With all the attention formal verification has been getting lately, particularly at the intersection of AI, theorem proving, and programming languages, we decided to put together FVjobs, a community-maintained job board to help people figure out who's actually hiring.

https://github.com/typetheoryforall/FVjobs

The board covers formal verification, proof engineering, automated reasoning, verified compilers, and AI-assisted theorem proving, among other related areas.

We're also keeping track of which tools companies use (Lean, Rocq, Isabelle, SMT, etc.), remote work options, and geographical restrictions. Hopefully, this makes it easier to find relevant opportunities without digging through dozens of company websites.

For now, we're keeping things simple with GitHub and GitHub Issues. Depending on how the project develops and whether there's enough community interest, we might eventually build a dedicated website.

This is a community effort, and we'd love your help keeping it up to date!

If you know of an open position, no GitHub knowledge is necessary. You can simply fill out this form:

https://github.com/typetheoryforall/FVjobs/issues/new?template=new-job.yml

Of course, issues and PRs are also very welcome.

Feedback and suggestions are appreciated, especially regarding what would make this resource more useful to the community!

After developing software for over 40 yrs, I’m implementing a new language specification, compiler, and standard library. Let’s assume it will have memory safety and some other features that modern languages have. This post is not a language announcement; it’s too early to release, but is coming soon.

My question is - for all of you that are designing or implementing your own, or for those who wish they could - what are the two or three features that you wish your daily-use language(s) had that they don’t today?

\- better documentation?
\- a better package manager?
\- better threading support?
\- better debugging tools?
\- better memory management?
\- better leak detection?
\- better integration with dev tools?

I’m genuinely curious and would love to hear your top wish list items.

TSP is an open standard that extends LSP – the Language Server Protocol that underpins editor integrations across the industry – designed to allow any editor or tool to integrate type checkers as first-class backends.

The initial use case is to enable changing the type checker powering Pylance (Microsoft's VS Code extension for Python) from their own Pyright to Meta's Pyrefly.

I think it's somewhat niche, but could be useful in situations like: - Enable switching between different compiler versions during full rewrites - When a language has multiple competing implementations and no single official type checker/compiler (as is the case with Python)

I've been making a programming language for a while now, and just came up with this idea for a feature i'm bout to implement. Patterns.

   pattern P {
    N;
    T(int, int);
    S {
        int x;
        int y;
    };
}
struct MS {
    int x;
}
class C {
    C() {}
    int y;
}
MS fits P(self) {
    N if (self->x == 0);
    T(self->x, -self->x) if (self->x < 10);
    S {
        x: self->x;
        y: 0;
    } if (self->x < 20);
    default N;
}
C fits P(self) {
    default N;
}
int main() {
    C c = C();
    c.y = 0;
    MS ms = {19};
    match (c) {
        P.N => `qout("Worked");
        default => `qout("Failed");
    }
    match (ms) {
        P.S {x, y} => `qout("Worked");
        default => `qout("Failed");
    }
    return 0;
} 

Basically, making user types have the ability to have custom behavior + extraction in match stmts, beyond just enums & integer types

apparently there isn't a low level language (likeC, C++, rust, obj-C.....the speedy languages you can think of) that prevents agents from corrupting the files by default, --
when the agent unexpectedly stops , all edits are made, and it's annoying to get the original state back, especially C/C++ family, one segmentation fault , never fixed, a lot of prompts , and burn all tokens
Is it possible to theoretically stopping hallucination , corruption , memory bugs at the language level for agents, and also make it llm friendly by default?

I have some ideas:

- compiled language seems to be more efficient, less prompt needed, rather than users finding bugs when they run, all obvious errors cached in the agent loop?
- checkpoint functionalities of compilers-- a command to return last state of successful build?
- decrease number of keywords?
like while/for -> loop?
function/procedure -> f?
const/var -> = (like python)

welcome any new ideas , or disagreement 😄

Hi everyone,

I've been working on I, an experimental systems programming language focused on low-level control, binary data representation, memory layouts, and systems programming.

The project includes a compiler written in C, code examples, documentation, and VS Code integration.

My goal is to explore a language design that makes low-level operations explicit while investigating how safety, predictable behavior, and hardware control can work together.

I'm sharing the project to get technical feedback on the compiler architecture, language design, testing strategy, and areas that need improvement.

GitHub: https://github.com/black-210/I

I'd particularly appreciate feedback on what would be needed to make this a practical language for systems programming.

for example:

fn pow(x : f64, n : i32) -> f64 { return mlir!( inputs : (%x = x : f64, %n = n : i32), returns : f64, dialects : \["math"\]) { %r = math.fpowi %x, %n : f64, i32 macro.yield %r : f64 }; }

Here the math.fpowi lowers to llvm.intr.powi so there is no need to implement pow as one in math.h of libc. Are there downsides of supporting mlir first class in a compiler?

i’ve been working on this for a while and it’s finally at a point where i can show it. it’s called go2js, it takes go code and spits out javascript you can run in node or the browser.

it handles goroutines and channels, generics, defer/panic/recover, multi package projects with go.mod, and a decent chunk of the standard library (fmt, json, time, net/http and some more). there’s also a go2js test command that runs your normal _test.go files.

the way i test it is pretty simple, every test runs the same program once with real go and once as the compiled js, and the output has to match exactly. that’s basically my definition of done.

there’s a playground too, it runs the compiler as wasm in your browser. fair warning it only does the language core, no imports, so no fmt in there.

some honest stuff: it’s v0.1, it’s experimental, goroutines are cooperative so timing won’t match real go, and the generated js is not tiny because the runtime comes along with it. also the readme, comments and most of the tests were written with ai and then edited by me, i put that in the readme so nobody has to guess.

i know gopherjs exists, i’m not claiming this is better, i just wanted to see how far i could push it, and i wanted the output to stay readable.

repo: https://github.com/zenobiatranoss/go2js
playground: https://zenobiatranoss.github.io/go2js/

if you try it on some real code and it breaks, please tell me, that’s the most useful thing right now.

I ran 500 batch tests (50 aggressive tests per batch) and another 500 but this time there are 100 aggressive tests per batch, all the bugs found were fixed, it has a built in linker, and other new major features.

I am designing a language. I want memory safety without using a tracing garbage collector or having heavy runtime costs. I have been looking at the options and I would like to know how others have dealt with these tradeoffs.

The options I have looked at:

- Ownership and borrow checking (Rust-style): Zero runtime cost but the compiler must prove things and the learning curve and syntax friction are real. I am not a fan of Rusts syntax so I wonder if the same guarantees can be provided with a surface.

- Reference counting (Swift/Nim-style): Predictable and simple but you pay for increments and decrements on every copy and cycles need either weak references or a cycle collector.

- Tracing GC: Easy for the user. Pause times and memory overhead are the usual complaints. It is a fit if the language is meant for games or system work.

- Regions/arenas with escape analysis: Allocate in scopes and let the compiler prove that nothing escapes. Very cheap,. I am not sure how far escape analysis can go before it becomes too restrictive.

- Bounds checks and tagged or hardware‑assisted checks (like ARM MTE): Catch many errors at low cost but they are mitigations, not guarantees.

My current thinking is a mix arenas by default an ownership model for long‑lived values and bounds checks that can be elided when the compiler can prove them safe. I would like to know whether that is a direction or whether I am missing a well‑known approach.

Specific questions:

has anyone implemented escape analysis that stays useful without forcing annotations?

Is there a middle ground between full borrow checking and reference counting that does not reintroduce cycle problems?

for those who have shipped a memory‑safe language with overhead what would you do differently?

Links, to papers, languages or post‑mortems are very welcome :)

Hi r/compilers

I built Sydrogen as my serious attempt at a compiler. It is a typed C-style systems language written in Rust. It was called ForgeLang until I renamed it since a lot of hobby languages use that name.

I've stopped working on it. The last release is Alpha-7 and there won't be more from me. I'm posting in case someone finds it useful or wants to take it

What might be interesting technically:

The compiler has two backends. The native one writes x86-64 machine code directly. Produces ELF64 or PE32+ executables without calling an external linker. The Cranelift one writes an object file and links with cc.

Both backends share the parser, AST and semantic checks, which run in parallel with Rayon.

It includes a set of language features like Do/Catch/Finally/Throw and fixed-size arrays and tuples though not all of them work on both backends.

What's unfinished:

The native backend doesn't handle floats or collections yet so those programs fall back to Cranelift.

The Windows backend doesn't have a runtime for Print or Input yet.

Finally doesn't run when Stop or Skip leaves a protected block.

There are no tests I'd call thorough. The README lists more gaps.

If you want to fork it fix something or just read the code the repo and book are here:

Repo: https://github.com/AeroForger/Sydrogen

Book: https://aeroforger.github.io/Sydrogen/

I'm not asking for anything. If you have questions, about how the native backend works I'm happy to answer them in the comments as I can.

Repo: https://github.com/alexios-angel/compile-time-browser

This project is AI-generated. Every line of code and every one of its ~6,500 commits was written by AI coding agents, mostly Claude and GPT. I didn't write the code. I just decided what to build, and sometimes directed the agents on how it should work.

I'm posting it here to show how far AI coding has gotten.

What got built

• A browser engine in C++23, from scratch. HTML parser, CSS, layout, a software rasterizer, and its own JavaScript VM. The VM passes 96% of industry-standard JavaScript conformance tests. It opens real pages in a window.
• A compiler that takes plain JavaScript and writes plain C++: structs, classes, std::vector, RAII, no garbage collector, no VM. When it can't prove something about the code, it refuses with an error instead of guessing. (The C++ it writes is correct but hard to read. It's in SSA form, one variable per intermediate value.)

Hasn't this been done? Turning JavaScript into native code, yes, many times. Almost every attempt either bundles a JS engine with the program or turns every value into a generic "could be anything" type backed by a runtime. All other major implementations package a garbage collector with your compiled code. My compiler does the opposite: it only writes C++ it can type and own, and refuses everything else. It also comes with its own browser engine, so web page code calls straight into it.

It took about 3 months of my time and roughly $40,000 in total, between AI usage and cloud costs/machines.

Where it is now

It's an alpha, and as of this week, current AIs are not good enough to continue progress on the goal of compiling real-world programs. The browser works on a lot of pages. The compiler handles small programs completely, but big real-world scripts are still mostly refused. I've shut down the cloud services I was using and AI API's until the AI does get good enough to continue writing code for the project.

Maybe if I get enough extra cash flow, I will continue the project in the immediate future.

AMA about the workflow, the costs, or what the AI wrote (I barely understand most of the code myself).

I found the discussion really interesting and thought you all would too. Richard talks about a pure Roc implementation of libdeflate and how to do performance optimizations unique to Roc. From a compiler perspective this is really interesting as to achievd this level of performance there are many optimizations needed under the hood, e.g. to mutate in place or elide checks etc.

Hi everyone, I am quite new to work as a compiler engineer, but I am quite confident with my day to day loop (find optimization opportunities or fixing any broken stuff). Most of my work is on the backend (and also most of my knowledge).

However, sometimes I am lacking of intresting ideas to implement, I also (almost) never touch LLVM middle end, yet.

Often times, I am in the "now what ?" situation. I would love to know how to keep improving and get better at compiler engineering.

Thanks.

I'm building my own programming language! Currently working on the standard library and bug fixes. It's designed to aim for memory safety with easy C interoperability.