The Anti-Human Consequences of Static Typing • Hacker News Board

Re: The Anti-Human Consequences of Static Typing

#41

Post by themstheones » Mon, Aug 12, 2013, 9:25 PM UTC

Someone wrote: post #22

themstheones wrote: post #11

Earlier quoted context omitted.

There are only four options for removing a block of code you no longer want to use: 1. Add a comment around the whole block. This may not always work, as comments within the block may need to be removed. 2. Add string delimiters before and after the block, making the block an in-place string literal. This can be broken by strings within the block. 3. Use a goto statement to skip the block. This is a pretty good metho…

5) delete it from your code. You do have source control, so you will be able to recover the code later. If you want to leave evidence, add a comment: -- Removed Foo handling in revision ... because of ... That should be rare, though. For temporary disabling, I tend to do: const disableFooForDebugging = true if( disableFooForDebugging) That makes it easier to recognize and correct accidental checkins.

Sorry, I was attempting to be humourous. Obviously #5 is the right way to go. I can't remember ever pulling something useful out of a block of commented out code.

Re: The Anti-Human Consequences of Static Typing

#42

Post by freyrs3 » Mon, Aug 12, 2013, 9:31 PM UTC

jeapostrophe wrote: post #39

freyrs3 wrote: post #38

Earlier quoted context omitted.

> mathematical proofs are not based on logic Mathematical proofs are explicitly logical statements, if they aren't based in logic they aren't proofs by definition. Mathematical intuition is what leads us to ideas but it's only within the framework of formal reasoning that we "know" anything within mathematics. Poincare said it nicely: "It is by logic we prove, it is by intuition that we invent."

If you really believe this, you should try to translate any contemporary (published) mathematical proof into a real logic, like Coq. It is hard and people earn PhDs doing this because most proofs are so intuition heavy in the first place.

I have spent several months doing proofs in Coq, as well as in Isabelle. I contest conflating Coq with "real logic", it is perfectly possible to do rigorous proofs without the aid of a computer-aided proof assistant, if that wasn't the case then there wouldn't be any reason to trust the authors of the proof assistant in the first place.

Re: The Anti-Human Consequences of Static Typing

#43

Post by [deleted] » Mon, Aug 12, 2013, 9:31 PM UTC

terhechte wrote: post #32

Funny coincidence, just today I wondered if there's such a thing as a statically typed Lisp, and stumbled upon Racket with types [1] I think another good example of a optionally static typed language would be Julia, where you can add types, and if you add them, the compiler will try to leverage that information to optimize your code [2]. I've used dynamic and static languages mixed for most of my life (Javascript, Py…

[deleted]

Re: The Anti-Human Consequences of Static Typing

#44

Post by enupten » Mon, Aug 12, 2013, 9:32 PM UTC

Kliment wrote: post #13

Are there any languages that have a type mismatch warning rather than a type mismatch error? Something like how gcc warns about incompatible pointer types when compiling C programs, but lets you use them if you insist, but for all types?

A few implementations of Common-Lisp (like SBCL) do this already (not surprisingly), and I find it very useful to compile misbehaving programs (and having not being segfaulted upon). Once you verify function behavior with a bunch of test cases, you declare types everywhere in the code and set the compiler optimization to full.

Re: The Anti-Human Consequences of Static Typing

#45

Post by kbenson » Mon, Aug 12, 2013, 9:32 PM UTC

dragonwriter wrote: post #26

pdonis wrote: post #24

Earlier quoted context omitted.

Static typing stopped the compile because the program does something foolish. But static typing would also stop the compile in situations where mixing types was not foolish. Static typing says you must give a definite type to every variable and every expression; but that's not always the best way to write your program. (To take a simple example from Python, there are plenty of cases where you want a function to retur…

> To take a simple example from Python, there are plenty of cases where you want a function to return either a string, say, or None, depending on whether it is able to find a string meeting some set of criteria, and you can't use the empty string as your "not found" value because empty strings are semantically significant for your application. Static typing is not a problem here. Static type with an inadequate type s…

And that's the whole point of his post. Don't let strict adherence from static typing overshadow interesting new techniques from being developed when we don't use static typing. We can then go back and update our type models to allow that new usage. The first comment on the article (bottom of the list of comments) clarifies his purpose.

Re: The Anti-Human Consequences of Static Typing

#46

Post by bitwize » Mon, Aug 12, 2013, 9:36 PM UTC

Static typing is pro-human; I would call it even more humane than dynamic typing.

Vastly more type errors (i.e., conditions which cause the program not to hold the property checked by the type system) are caused by programmer error than by deliberate design; a strong, static type system, checked at compile time, helps ensure that a whole class of relatively weak but trivially easy to write bugs do not find their way into the finished program. The programmer hours saved in not having to worry that some little-exercised code path will attempt to add an integer to a string, nor to write exhaustive tests covering every possible code path to make sure no integers get added to strings, adds up significantly over the program's lifecycle, from initial development through maintenance and support.

Be kind to your programmers. Use a statically-typed language.

Re: The Anti-Human Consequences of Static Typing

#47

Post by bitwize » Mon, Aug 12, 2013, 9:37 PM UTC

zeidrich wrote: post #25

I agree, we need to have far more human compilers. Perhaps, when I compiler runs across a type violation it just breaks out laughing at you. "HA HA HA! You idiot! You defined this variable as a string, and then you tried to do arithmetic on it, WHAT WERE YOU THINKING?" Maybe the compiler can just complain about the user. "Seriously, this guy first gets me to make this integer, and that's cool, but then he starts to u…

a typedef name was a complete surprise to me at this point in your program

Re: The Anti-Human Consequences of Static Typing

#48

Post by pasquinelli » Mon, Aug 12, 2013, 9:39 PM UTC

"Advocates for static typing are anti-human, because they argue that the only programs we should allow to run are the ones that have been verified by machines! In contrast, the freedom fighters contra to these typing terrorists argue that humans can perform analysis and decision making as well!"

humans suck at verifying programs.

let's keep going with this, why do we only consider a program to be running when it's running on a machine!? humans can run programs as well!

Re: The Anti-Human Consequences of Static Typing

#49

Post by dragonwriter » Mon, Aug 12, 2013, 9:40 PM UTC

Permit wrote: post #20

>The logic goes that if you reject "bad" programs then only "good" programs remain, and who would want to run "bad" programs anyways? I thought the logic was: if you reject all bad programs and some good programs, only good programs remain, is it not?

I think the logic actually goes "if you reject upfront all programs with a certain type of badness as well as some programs that falsely appear to have that type of badness, you will reduce the costs associated with bad programs by catching many of them sooner, at the cost of having to rewrite some already-good programs in less-simple ways to avoid the appearance of badness."

Re: The Anti-Human Consequences of Static Typing

#50

Post by hcarvalhoalves » Mon, Aug 12, 2013, 9:48 PM UTC

> (+ 1 > (if (negative? (fahrenheit->kelvin (abs some-number))) > "2" > 2))

This is inconsistent code to being with, though. You can't guarantee it "never" reaches the first branch, as much as you can't guarantee there aren't bugs in the conversion function, or on the underlying interpreter, or that machine details wouldn't make a big enough number wrap around and return negative. All in all, an inconsistent code branch hanging around is a bug even if it compiles.

This is more an evidence that "if" is evil rather than an argument about typing, really.