Comment by pron

Comment by pron 3 hours ago

Not really. With dependent types, you can have a function that returns a type that depends on a runtime value; with Zig's comptime, it can only depend on a compile-time value.

Note that a language with dependent types doesn't actually "generate" types at runtime (as Zig does at compile-time). It's really about managing proofs that certain runtime objects are instances of certain types. E.g. you could have a "prime number" type, and functions that compute integers would need to include a proof that their result is a prime number if they want to return an instance of the prime number type.

Using dependent types well can be a lot of work in practice. You basically need to write correctness proofs of arbitrary properties.

CoastalCoder 2 hours ago

Sorry if this is obvious, but do these languages let programmers explicitly assert that a certain, relevant property holds at runtime?

Or do these compilers insist on working these proofs out on there own without the benefit of programmer-supplied assertions?

Reply View 2 replies

pron an hour ago

> do these languages let programmers explicitly assert that a certain, relevant property holds at runtime?
Yes, but the programmer has to do the really, really, really hard work of proving that's the case. Otherwise, the compiler says: you haven't proved to me that it's true, so I won't let you make this assertion. Put another way: the compiler checks your proof, but it doesn't write it for you.
The only programs for which all interesting assertions have been proven in this, or a similar, way have not only been small (up to ~10KLOC), but the size of such programs relative to that of the average program has been falling for several decades.

Reply View | 0 replies
naasking an hour ago

> Sorry if this is obvious, but do these languages let programmers explicitly assert that a certain, relevant property holds at runtime?
You can assert something but then you also have to prove it. An assertion is like a type declaration: you're asserting values of this type can exist. The proof of that assertion is constructing a value of that type to show that it can be instantiated.
This is what the Curry-Howard correspondence means. The types of most languages are just very weak propositions/assertions, but dependent types let you declare arbitrarily complex assertions. Constructing values of such arbitrarily complex assertions can get very hairy.

Reply View | 0 replies