4 ms·

I've never hated a piece of software with the same burning passion I reserve for Coq, but I'm happy to see they are still around releasing new way to brutalize

by frollo 6y ago

I've never hated a piece of software with the same burning passion I reserve for Coq, but I'm happy to see they are still around releasing new way to brutalize the mind of the unprepared.

deathtrader666 6y ago
Alright, but why?
- Tyr42 6y ago
  I used it, and while I didn't hate it, I can totally see why it could inspire someone to write such a comment.
tluyben2 6y ago
Why is that? And what alternative do you prefer? I do not mind it for what it is meant for. I rather would have it more practical (instead of having to write software twice: once to prove it and once to execute it), but that is also very new and experimental, like F* or Idris.
- frollo 6y ago
  As I said before, it was mostly because it used to crash a lot for weird reasons (I think it didn't really like something in my laptop's memory) and the only explanations I ever got were in French. If they finally finished translating the documentation and the errors (or fixed whatever memory weirdness was affecting my version) it wouldn't be so bad. I'd still hate it from the countless sleepless night trying to get it start again before the weekly assignment's deadline, though.
tobmlt 6y ago
This is a beautiful, dark humored, hilarious comment. Thanks for it!
bidirectional 6y ago
I'd be interested in hearing why, or at least hearing the context behind it (i.e. there's a big difference between an undergrad forced to use it for a project and a dependent types researcher who prefers Lean)?
- frollo 6y ago
  It was about 4 or 5 years ago, when I was in grad school. The main problem I had with it is that it kept crashing or failing for misterious reason and it just printed out some obscure French error message (which I was forced to pass through Google Translate, since nobody in the whole class could speak French). This only happened for the most obscure errors, while the more common and easy to spot ones (logical errors, typos...) were well documented in English. Also a lot of useful parts of the manual (and the community posts around it) were written in French. I don't think it's really inferior to other tools, but the bad documentation and tendency to crash (which I hope had been fixed by now, TBH) got on my nerves.
  - julienreszka 6y ago
    Liar
  - tom_mellior 6y ago
    Lest anyone read this and fear that this is common: In my experience it isn't. Nor was it 4 or 5 years ago. I've never seen Coq crash at all, nor spit out any error message in French, and I was a full-time user for a while.
    - frollo 6y ago
      In my recollection (but I could have read it wrong the first time) it tied to the OS. It had those problem on Linux, but both Mac and Windows users were capable of running it without much hassle (although they did experience the occasional crash). Also, people running Arch had less problems than us running Debian. But I just wanted to pass the course and didn't spend much time debugging it, so it could have been another thing (just a couple of ideas from the top of my head: library versions, conflicts with other running programs, some compiler weirdness...)
deleted 6y ago
[deleted]
mbrodersen 6y ago
I have never ever seen it crash.

by frollo 6y ago

I've never hated a piece of software with the same burning passion I reserve for Coq, but I'm happy to see they are still around releasing new way to brutalize the mind of the unprepared.

deathtrader666 6y ago

Alright, but why?

Tyr42 6y ago
I used it, and while I didn't hate it, I can totally see why it could inspire someone to write such a comment.

tluyben2 6y ago

Why is that? And what alternative do you prefer? I do not mind it for what it is meant for. I rather would have it more practical (instead of having to write software twice: once to prove it and once to execute it), but that is also very new and experimental, like F* or Idris.

frollo 6y ago
As I said before, it was mostly because it used to crash a lot for weird reasons (I think it didn't really like something in my laptop's memory) and the only explanations I ever got were in French. If they finally finished translating the documentation and the errors (or fixed whatever memory weirdness was affecting my version) it wouldn't be so bad. I'd still hate it from the countless sleepless night trying to get it start again before the weekly assignment's deadline, though.

tobmlt 6y ago

This is a beautiful, dark humored, hilarious comment. Thanks for it!

bidirectional 6y ago

I'd be interested in hearing why, or at least hearing the context behind it (i.e. there's a big difference between an undergrad forced to use it for a project and a dependent types researcher who prefers Lean)?

frollo 6y ago
It was about 4 or 5 years ago, when I was in grad school. The main problem I had with it is that it kept crashing or failing for misterious reason and it just printed out some obscure French error message (which I was forced to pass through Google Translate, since nobody in the whole class could speak French). This only happened for the most obscure errors, while the more common and easy to spot ones (logical errors, typos...) were well documented in English. Also a lot of useful parts of the manual (and the community posts around it) were written in French. I don't think it's really inferior to other tools, but the bad documentation and tendency to crash (which I hope had been fixed by now, TBH) got on my nerves.
- julienreszka 6y ago
  Liar
- tom_mellior 6y ago
  Lest anyone read this and fear that this is common: In my experience it isn't. Nor was it 4 or 5 years ago. I've never seen Coq crash at all, nor spit out any error message in French, and I was a full-time user for a while.
  - frollo 6y ago
    In my recollection (but I could have read it wrong the first time) it tied to the OS. It had those problem on Linux, but both Mac and Windows users were capable of running it without much hassle (although they did experience the occasional crash). Also, people running Arch had less problems than us running Debian. But I just wanted to pass the course and didn't spend much time debugging it, so it could have been another thing (just a couple of ideas from the top of my head: library versions, conflicts with other running programs, some compiler weirdness...)

deleted 6y ago

[deleted]

mbrodersen 6y ago

I have never ever seen it crash.