Are programmers biased in terms of spending more time writing code than they do thinking about it?
Yes, the importance of thinking and writing before you code needs to be taught in undergraduate computer science courses and it’s not. And the reason is that there’s no communication between the people who teach programming and the people who teach program verification.
Schlagwort-Archiv: Programmieren
Thinkoding.
Lean.
Is it still a proof if it takes 4 minutes on a 4 GHz 12-core CPU?
Tetreassuring.
Summary: it is possible to play Tetris and guarantee that you will score at least one line, no matter which pieces are given to you, i.e., even assuming they are chosen adversarially.
Uniband.
Some artists will benchmark your utf8 support: [...]
dustri.org: Horrible edge cases to consider when dealing with music
Only quoted.
Beware of bugs in the above code;
I have only proved it correct, not tried it.
Peta reduce.
1990 - A committee formed by Simon Peyton-Jones, Paul Hudak, Philip Wadler, Ashton Kutcher, and People for the Ethical Treatment of Animals creates Haskell, a pure, non-strict, functional language. Haskell gets some resistance due to the complexity of using monads to control side effects. Wadler tries to appease critics by explaining that "a monad is a monoid in the category of endofunctors, what's the problem?"
One Div Zero: A Brief, Incomplete, and Mostly Wrong History of Programming Languages
Leanorris.
Hey! I heard that Lean thinks 1/0 = 0. Is that true?
Yes. So do Coq and Agda and many other theorem provers.
[...]
But doesn’t that lead to confusion?
It certainly seems to lead to confusion on Twitter. But it doesn’t lead to confusion when doing mathematics in a theorem prover. Mathematicians don’t divide by 0 and hence in practice they never notice the difference between real.div and mathematical division (for which 1/0 is undefined). Indeed, if a mathematician is asking what Lean thinks 1/0 is, one might ask the mathematician why they are even asking, because as we all know, dividing by 0 is not allowed in mathematics, and hence this cannot be relevant to their work.