Follow

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.

Friendly reminder regarding CoCs 

@raichoo This is like saying that are no bad rules.

Friendly reminder regarding CoCs 

@murks @raichoo

"Rules for behavior are good unless you like behaving badly"

"Wow I guess you think all rules are always good"

#ICanHazLogic

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 

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

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

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