Comment by lmm | Hacker News Reader

Comment by lmm | Hacker News Reader

Parent Full thread

> 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?

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).

Reply on news.ycombinator.com