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


Crossing the streams, joke 

@raichoo @juliobiason As things are now, I agree. Well, except there's a lot of core modules that should be proven in Coq and extracted to ML (or any similar flow).

But looking at the state of software generally, we need to push harder to get the computers to do more work for us, especially the things humans are bad at.

Crossing the streams, joke 

@tfb @juliobiason I agree. But let's be frank, for most of the industry things like ML are obscure technologies. Haskell made some ground in the last couple of years but still. DTs are relatively fringe, even in academia. Also, technology can also solve a fraction of the problem. A lot of developers just don't care about code quality or lack a basic understanding of the tools they are using.

Sign in to participate in the conversation
Functional Caf茅

The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!