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

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

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.

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