580 reputation
28
bio website
location Cologne, Germany
age
visits member for 3 years, 6 months
seen 6 hours ago

Functional programming enthusiast, audio engineer & musician. Whilst not busy with any of that, I study physics at Universität zu Köln / Bonn-Cologne Graduate School.


2d
comment Are all magic numbers created the same?
The ideal way to eliminate magic numbers is to make the literal itself unnecessary. In this case: store such sizes not in integer variables but in a type-system enforced variable of some physical-dimension type Information. In an OO language that would be a class with methods to output readings in specific prefix, or as a string with automatically-chosen prefix ("human-readable"). But the conversion by multiplication / division should never appear anywhere openly. (Admittedly, what I'm describing is still a bit of a utopia.)
2d
comment Are all magic numbers created the same?
@LightnessRacesinOrbit: I could bet that somebody used #define BYTES_PER_MBYTE 1024*1024 somewhere, and later wondered why they got MBval ≡ byteVal...
Dec
12
comment Is there something as a bug-free application?
(Again, there are concepts like STM which allow some proofs even in concurrent systems, but that also has its limits – any setting in which you want to proove something needs a well-bounded scope; the actual physical world simply is not a well-defined mathematical setting.)
Dec
12
comment Is there something as a bug-free application?
@Giorgio: well, looping forever might be correct for some application. Then, of course, terminating would probably be a bug! Real-world applications have of course specifications, often somewhat "fuzzy" ones, but obviously some behaviours are just wrong. I'm not going to boil up some particular example here, but IMO the point is really obvious given the complexity of many real-time systems, in particular when concurrency is involved, and many parts depend on something to be ready at a given time. Such a system can break in all kinds of ways, simply because some function takes a bit too long.
Dec
12
comment Is there something as a bug-free application?
@JanDvorak: basically, yes. And as I said, in an "ordinary" static-types language, this is not really sufficient to proove correctness. But in a dependently-typed language, you can in fact refine your types so they'll only match in a thoroughly correct program. ("Thoroughly", of course, again ignoring real-world runtime and similar dirt.)
Dec
12
comment Is there something as a bug-free application?
@Giorgio: dunno, but for sure similar loops can be found in lots of production applications.
Dec
12
comment Is there something as a bug-free application?
@Giorgio: the condition is "there is no new post on StackExchange I haven't processed yet".
Dec
12
comment Is there something as a bug-free application?
@JanDvorak: it's an official usage of the term "proven". You make some mathematical statement in form of a type signature, and then the implementation prooves that the statement was correct. Mind, those statements generally don't look much like function signatures as you would find in real-world programs.
Dec
12
comment Is there something as a bug-free application?
@Giorgio: easy, loop over all StackExchange post that can be found. Might terminate if the loop body is faster than the next poster, or might loop forever as long as new posts keep coming in faster than you can process them.
Dec
12
comment Is there something as a bug-free application?
@JanDvorak: well, if you swap a plus for minus, a dependently-typed language can still proove whether it's "correct"... only, "correct" might then refer to a different theorem.
Dec
12
comment Is there something as a bug-free application?
@Giorgio: yes, for recursion you can beautifully apply inductive proofs. But that prooves only the functional specification, it doesn't tell you anything about how long it might take (the induction might basically reach to infinity). — That point was in fact pretty much the gist of my answer, wasn't it?
Dec
12
comment Is there something as a bug-free application?
@Giorgio: sure you can write some programs in a way that allows such a verification, but that really restricts you quite a lot. In a big program, you'll almost always need to exploit Turing completeness somewhere. — Yes, in practise you specify, code and "verify" simultaneously, but that verification is often enough heuristic (based on e.g. unit tests, not real proofs).
Dec
12
revised Is there something as a bug-free application?
added 443 characters in body
Dec
12
answered Is there something as a bug-free application?
Dec
4
comment Which are the cases when 'uint' and 'short' datatypes are a better fit than the standard int(32)?
"benefit is memory space and cpu time"... I don't see any case where tiny-types would actually save CPU time. Integer operations never get faster than they are on the machine-sized types, i.e. as far as CPU is concerned you might as well use long. Memory saving can of course indirectly save time by improving cache-line efficiency and so on, but OTOH the alignment issues with small types can indirectly cost time.
Oct
27
comment What can Haskell's type system do that Java's can't and vice versa?
I wouldn't call ADTs a feature of the type system. You can fully (if awkwardly) emulate them with OO wrappers.
Oct
22
comment Why are floating point numbers used often in Science/Engineering?
That quote being from here. A good read and plenty to discuss about, but not here since indeed it has nothing to do with your post or this question.
Oct
4
comment Is there an optimal number of lines of code per function?
Nᴏʙᴏᴅʏ expects the Spanish... ah bugger, I'm a bit late here.
Sep
28
comment Why is type inference useful?
Well, technically, the information is always redundant when it's possible to omit manual signatures: otherwise the compiler wouldn't be able to infer them! But I get what you mean: when you just duplicate a signature to multiple spots in a single view, it's really redundant to the brain, while a few well-placed type give information you'd have to search a long while, possibly with a good many nonobvious transformations.
Sep
28
comment Why do most programming languages have special keyword or syntax for declaring functions?
"Mathematicians don't prefer f = nn + 1 over f (n) = n + 1" ... Not to mention physicists, who like to write only f = n + 1 ...