Alperen Keleş

Finally updated the interface for my puzzle!
puzzle.alperenkeles.com/leaderboard

Breaking Verifiable Abstractions and going beyond prompting👇🏻
alperenkeles.com/posts/verifi...

I wrote about a topic that I wanted to do for a very long time. Here's A Better Vocabulary for Testing.
alperenkeles.com/posts/vocab-...

#BOBkonf2025 talk "Property-Based Testing: The Past, The Present, and The Future" by @keles.bsky.social is up on our website!
bobkonf.de/2025/keles.h...

Here it is
smt.st

There’s a great book with lots of practical examples, let me find that

Ah no, it would break early in the first type error. This is slow for cases it is well typed. The other is slow for cases it is ill-typed.

Because constraint solvers are better at falsifying constraints then proving them. Falsification means you can stop halfway when you produce a falsifying model to the problem.

You could do the reverse, and tell it “I bet you can find a set of assignments that satisfies it”, so it will return SAT indicating well-typedness and UNSAT + breaking constraints, but that tends to be slower than the reverse as far as I know.

I think it gets untractable really really fast. This was my undergrad graduation project, so we didn’t have a lot large programs we could test it with, but even the call to Z3 is very slow compared to classic type checking

So you either need to modularize the type checking and somehow make it incremental, or have some type of hybrid approach.

The problem, of course, is type errors. Because if Z3 really cannot find a set of assignments that works, it just tells you yes, you are correct, but you don’t get a local type error for it.

Yeap, you produce constraints for every variable based on their use sites, definitions etc. and then you tell Z3 “I bet you can’t find a set of assignments for these constraints”, at which point it gives a set of types assigned to variables as its result.

My first type checker was entirely Z3 driven, we had Dafny style requires/ensures annotations proven via Z3, so that played nicely. The typed jq type system might also switch to Z3 at some point, not sure yet

I've written some of my thoughts on the capabilities and limits of LLMs for Programming.

Verifiability is the Limit | alperenkeles.com/posts/verifi...

Does anyone have any articles on pretty printing in Rust? `pretty` crate is surprisingly under-documented.

Paylaştım abi sitede alperenkeles.com/posts/tip-si...

Tip Sistemleri Hakkında 👇🏻

alperenkeles.com/posts/tip-si...

Tip sistemleri hakkında 15 sayfalık Türkçe bir mini-makale yazdım, okuyup yorum yapmak isteyen var mıdır acaba? Araştırabildiğim kadarıyla yayınlanırsa şu zamana kadar yazılmış Türkçe en kapsamlı kaynak olacak, güzelce detaylandırabilmek istiyorum.

Alperen (alperenkeles.com) is speaking at next month’s DC Systems about what’s out there for Property-Based Testing, and more importantly, what isn’t there yet.

He will talk about what the latest research on PBT is, and how we can bring it to the mainstream libraries.

Don’t miss:
dcsystems.xyz

Abi ben bir şeyi sevip ona odaklanabileceğim inancını bıraktım bayağı bir süre önce. Canımın istediği şeyleri yapıp paralel ilerlemeye çalışıyorum, bir tane ana yol belirleyip kendimi de zorluyorum sadece en çok vakti buna harcayacaksın diye.

I'm implementing a `trace` macro for creating custom stack traces following only the functions you care about. It basically gives you a debugger post-hoc, hopefully an improvement over printf-debugging.
pbs.twimg.com/media/GdBXjZ...

THERE'S A LANGUAGE FILTER?? I may actually use this site

github.com/alpaylan/tjq

A prototype type inference engine for jq

Learner’s Guide to Functional Programming#0: Sum Types, Booleans and Naturals in Javascript After writing the first article of the Learner’s Guide to Functional Programming series yesterday on implementing functional lists, I have…

Learner’s Guide to Functional Programming#0: Sum Types, Booleans and Naturals in Javascript

"...implementing functional lists, I have realized I may have jumped in too fast..."

Learner’s Guide to Functional Programming#1: Implementing Lists in JavaScript There are many articles introducing functional programming. They mention immutability, first class functions, purity, recursion, and many…

Learner’s Guide to Functional Programming#1: Implementing Lists in JavaScript

"...We will implement functional data structures within using a very minimal subset of Javascript. No loops, no mutable variables, no builtins except primitive types..."

Extracting Signals: Playing The Inverse Waldo Game I believe most of you will recognize the game in the following image, “Where’s Waldo?”. It has many variations such as finding the cat, the…

Extracting Signals: Playing The Inverse Waldo Game

"...Creating content is like playing an Inverse Waldo Game. High quality content reduces noise, guides the reader throughout the signals it tries to convey..."

Bu site biraz kendini düzeltmezse zor. UI çok kötü, az önce yanlışlıkla translate'e bastım sizin tweette Google translate açtı yeni pencerede

600 posts a day, alright I’m done with that now

Elon siteyi tamamen bozduğuna göre burdan devam etmenin vakti gelmiş gibi