Friendly reminder regarding CoCs 

If you think a CoC is a problem you
a) are part of the problem that CoCs are trying to address
or
b) have been successfully gamed by people who are part of the problem into being their tool.

Crossing the streams, joke 

@raichoo @juliobiason Of course CoC is a problem, we should obviously be using the Calculus of Co-Inductive Constructions!

(I agree about your use of CoC, but it's not how I parsed it 馃槀)

Hey this is an actually good use is a CW!

Crossing the streams, joke 

@tfb @juliobiason That's fine, we are doing this CoC joke all the time :)

Crossing the streams, joke 

@raichoo @juliobiason In which case ... Your post stands just fine with either parsing of CoC. The reluctance to put dependent types into production is its own problem...

Crossing the streams, joke 

@tfb @juliobiason Having hacked quite a lot on the Idris compiler as well as trying out all sorts of stuff in that language, I believe that reluctance is currently justified. DTs are great but for most of the programming I do on a daily basis, Haskell98 is almost always enough.

Follow

Crossing the streams, joke 

@tfb But that's such a lengthy discussion, and social media always seems to be the wrong place for that 馃樅

Web 0 0 1
Sign in to participate in the conversation
chaos.social

chaos.social 鈥 a Fediverse instance for & by the Chaos community