4 ms·

I've spent some time pondering things like that, but ultimately concluded that we should keep these things away because there is a duplication between type-leve

I've spent some time pondering things like that, but ultimately concluded that we should keep these things away because there is a duplication between type-level and code level, and I'm completely fine with sprinkling a few runtime assertions in most cases. Normal code syntax is much more suited to expressing invariants. Obviously I'm not into statically proving the correctness of my programs, so if that's your cup of tea things are probably looking different (and I'm sorry for you).

atq2119 5y ago
I would love to be able to do more formal proving of programs in practice, but I 100% agree with you. A lot of what the advanced typing crowd seem to be doing is to re-invent programming but at the type level, and it's unclear to me why that should count as progress. It reminds me uncomfortably of C++ template metaprogramming -- and for good reasons, C++ has made steps towards replacing that with statically evaluated expressions written in regular syntax. My gut feeling is that the right way forward is to have a fairly standard type system visible in the source language augmented by contracts written in regular code. Basically a slight augmentation of assert(). A formal prover could internally reason about an extended type system where those contracts are automatically lifted to the type level if that helps for some reason, but programmers wouldn't be bothered with it. This seems unlikely to be a genuinely novel idea, so I'd be curious to hear whether systems like that already exist.
- captainmuon 5y ago
  Exactly. It pains me when someone comes up with a new language with dependent types, but then to encode a simple constraint they first define integers via peano axioms using some kind of template metaprogramming. (The example I'm remembering was Coq or a Haskell dialect or something.) There was a dialect of C#, Sing# or Spec#, that allowed you to specifying pre and post conditions in the same expression language as the main language, and they were checked at compile time. This is what comes closest I think.

atq2119 5y ago

I would love to be able to do more formal proving of programs in practice, but I 100% agree with you. A lot of what the advanced typing crowd seem to be doing is to re-invent programming but at the type level, and it's unclear to me why that should count as progress. It reminds me uncomfortably of C++ template metaprogramming -- and for good reasons, C++ has made steps towards replacing that with statically evaluated expressions written in regular syntax. My gut feeling is that the right way forward is to have a fairly standard type system visible in the source language augmented by contracts written in regular code. Basically a slight augmentation of assert(). A formal prover could internally reason about an extended type system where those contracts are automatically lifted to the type level if that helps for some reason, but programmers wouldn't be bothered with it. This seems unlikely to be a genuinely novel idea, so I'd be curious to hear whether systems like that already exist.

captainmuon 5y ago
Exactly. It pains me when someone comes up with a new language with dependent types, but then to encode a simple constraint they first define integers via peano axioms using some kind of template metaprogramming. (The example I'm remembering was Coq or a Haskell dialect or something.) There was a dialect of C#, Sing# or Spec#, that allowed you to specifying pre and post conditions in the same expression language as the main language, and they were checked at compile time. This is what comes closest I think.