[jstimpfle]

Typical invariant for me would look like:

Given a, b, c input parameters to my func, it must hold that that a->m->t == b->t. c->mutex must be held, and c->cond is the condition variable that goes with c->mutex and will release any waiters on the buffer contained in a.

Or: Integer x is representable using 12 bits only, Integer y should be a multiple of N and I have a integer s is used as a bit-shift that should be less than 8.

Or: I need to guarantee that no locks have to be taken and no allocations have to be made on this complicated looking codepath. While holding a lock, we must not do any syscalls (syscall a, b, c are ok though), and surely not make any logging calls.

I know only one system that can express this, it's called STRAIGHTFORWARD CODE, and it requires doing engineering and casual logic out-of-band, and yes it does include making mistakes and repairing them incrementally.

I don't know a type system that would let me explain these things to me and tell me where I was wrong. But maybe you can show me, with 5 minutes of actually trying?

[lmm]

> it must hold that that a->m->t == b->t.

So define a wrapper type that represents that invariant (it's not going to take up space at runtime), where the only constructor enforces it?

> Integer x is representable using 12 bits only, Integer y should be a multiple of N and I have a integer s is used as a bit-shift that should be less than 8.

Those are all standard things that already exist?

> Or: I need to guarantee that no locks have to be taken and no allocations have to be made on this complicated looking codepath. While holding a lock, we must not do any syscalls (syscall a, b, c are ok though), and surely not make any logging calls.

Sounds like a pretty standard free monad case? Define a command algebra in which the "ok" syscalls are a subtype, and then require that the thing you want to only use the ok calls to have a type that reflects that?

[jstimpfle]

Please, go ahead and type the example. I think you are trolling.

> Define a command algebra in which the "ok" syscalls are a subtype

Dude, it's clear you're not doing any actual work. You are living in an ivory tower, and you underestimate the complexity and detail and volatility of real world applications by at least 3 orders of magnitude. You don't understand how to modularize and contain complexity.

You _cannot_ complete a project with this attitude.

You are ignorant of the fact that a type system is necessarily a blunt simplification of the real complexity. Therefore, use of types must be pragmatic, and actual logic must be coded in normal code (which should be obvious but it isn't to type theory weirdos). Otherwise, you require dependent typing or whatever, and you will have to write your code twice, once in a usable programming language and once in a very unusable programming language. Much more than only twice actually, given that all the implicit detail should apprently go explicitly formalized at the type level.

Just to make sure I'm not entirely talking out of my arse because I'm so incredibly annoyed by your otherworldly proposition, I asked an AI about the sel4 microkernel. It consists of 10,000 lines of C code (that says a lot about its practical utility, which is very limited), and of 1,3 million lines of manually written proof code (which says a lot about the practicality of proving).