beautiful code

Beautiful code. I want to create it. How can i do this?

https://news.ycombinator.com/item?id=7234855

>>39
I've tried so hard man, it's near impossible to write even simple programs with full correctness proofs. Partly because the tools aren't good enough.

>>34

Also, enjoy your strict evaluation and rampant side effects. Mutable ref cells are also an obvious piece of shit.

hahahahaha fuck off back to #haskell you fucking fanboy

>>42

Yeah, it is hard, the techniques are not there yet. I think constructive logic is partly to blame. Most mathematics use non-constructive logics to prove stuff.

>>42

And totality can be a bitch.

>>45
That's why I want a non-total dependently-typed language. You get correctness where you want it (i.e. with types like Array SortedAscending 256 Int) and simplicity in other places (SimpleArray Int) without having to prove termination, thus without having to be stuck with structural recursion and having to write pages of stupid proofs.

>>46
Idris might be interesting, but it is als not there yet. It has optional totality built in. There is little theoretical foundation though, so that might be a problem.

>>33
and fix global interpreter lock.

>>48
Yeah, that is annoying.