3 ms·

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 in

• naasking 11mo 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.
• pron 11mo 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.