catnaroek

9 ms·

31.
by catnaroek 9y ago
I can't prove anything about programs other people will write, unless the language itself makes guarantees about the programs they can write. Culture doesn't help one iota.
32.
by catnaroek 9y ago
> Even if their encoding has identify, immutable value don’t need it. Values indeed don't have physical identities. The problem is that, when you use a language with pervasive object identities, the values you want only exist in you
33.
by catnaroek 9y ago
> Immutable objects do not have identity and are values. Really? https://ideone.com/mmQJGr > And the distinction between primitives and objects in Java, for our discussion here, is irrelevant. All it takes to disabu
34.
by catnaroek 9y ago
> Java's semantics permit defining pure functions, immutable values Only by social convention. Not enforced by the language's semantics in any meaningful way. In fact, Java does not even allow the programmer to define custom va
35.
by catnaroek 9y ago
Sure, but that would be an object language embedded in the lambda calculus, not the lambda calculus itself. btw, variants of the lambda calculus do exist where some values (so-called “reference cells”) are object identities. But a value c
36.
by catnaroek 9y ago
Closures are simply an implementation detail of first-class procedures. But functional programming, unlike object-oriented programming, isn't just about making procedures first-class. It's about using, to the greatest extent possi
37.
by catnaroek 9y ago
> Lisp was based on the lambda calculus, not sure if you can get more functional than that. I've tried really hard (okay, for about five minutes), but couldn't find any account of the lambda calculus that includes the following
38.
by catnaroek 9y ago
> Functional Programming is programming with mathematical functions (aka pure functions). Exactly. To which the following must be added: Functions are mappings from values to values. It makes no sense to try to do functional programming
39.
by catnaroek 9y ago
Even if your dependencies are not formally verified, it is useful to formalize your expectations of them.
40.
by catnaroek 9y ago
Theorem: Whenever `numbers[index]` is used, `0 <= index < numbers.length`. Proof: Use the loop invariant `0 <= index <= numbers.length`. The invariant holds before the loop begins because `index == 0` (established by you) and `n
41.
by catnaroek 9y ago
> I've never yet had the luxury of working in a language that admitted formal proofs of correctness. You don't need much from your language, except for a formal semantics. But, even if your language of choice doesn't have
42.
by catnaroek 9y ago
Yes. This is the only way you can justify that you know better than the compiler.
43.
by catnaroek 9y ago
What I need is the proof that the program is correct. Bugs will show up as gaps or inconsistencies in the proof. But, in the absence of even an attempt at a proof, all I can do is throw the program to the dogs.
44.
by catnaroek 9y ago
> in JavaScript, not all values are immutable. Object states are mutable, of course. But they are not values. You can't bind object states to variables. If you use objects as proxies for values that exist in your head but not in i
45.
by catnaroek 9y ago
Stack traces contain a lot of information. Most of it is useless garbage. Yet at the same time sometimes stack traces don't contain the information you need. Making them even more useless garbage.
46.
by catnaroek 9y ago
This is a very good argument against mandatory automatic static checks, so long as they are replaced with equally mandatory manual proofs, included in the program's comments and/or documentation. But it does not justify dynamic ty
47.
by catnaroek 9y ago
> This is to say, I don't think inference and gradual systems are necessarily at odds, but could potentially work together, although that doesn't happen today. Type inference demands some rigidity in the type structure of a lan
48.
by catnaroek 9y ago
> where to hold state Wherever it makes the most sense for the algorithms you want to implement. > interactions between components Again, driven by the needs of the algorithms, and, most importantly, their proofs of correctness.
49.
by catnaroek 9y ago
> But it's clearly not what people mean when they talk about pointers (or references) being mutable. The semantics of a programming language is what it is, not what you want it to be, unless you explicitly choose a language that all
50.
by catnaroek 9y ago
Not every optionally typed system is gradually typed. The purpose of gradual typing is to allow typed and untyped code to interact (0) without destroying the safety guarantees of typed code, (1) correctly assigning blame, if a runtime type
51.
by catnaroek 9y ago
The argument for dynamic typing (whether one agrees with it or not, I actually don't) has nothing to do with explicit annotations. Rather, it is that there are paths in the design space that lead to correct solutions but pass through s
52.
by catnaroek 9y ago
> I wish I could do this with larger code bases but unfortunately, from my own experience, planning time is exponentially related to the projected lines of code. Hence more work has to be done on expressing solutions to big problems as t
53.
by catnaroek 9y ago
That's because the real value is the object identity, not its state. Trust me, object identities are immutable.
54.
by catnaroek 9y ago
Weird, for me it is exactly the other way around. The syntax might be familiar, but it is idiotic. On the other hand, the semantics is exactly what I have always wanted C++ to be.
55.
by catnaroek 9y ago
Stack traces are not a very good argument. As a general rule, you should write your programs to be flawless. Only if you are unsure about a particular piece of code, then can you manually add debugging information, at your own expense.
56.
by catnaroek 9y ago
Not a very good example. The n-th term of the Fibonacci sequence can be computed straightforwardly with an imperative loop: def mul(a,b,c,d): x = a*c + a*d + b*c y = a*c + b*d return x,y def fib(n):
57.
by catnaroek 9y ago
This suggests trying “scared that my wife and children will be executed if I do it wrong”.
58.
by catnaroek 9y ago
> What do you do about programming errors you cannot identify? A programming language designer can only do so much for you. If you cannot identify errors in your programs on your own, consider switching to a different career. > And wh
59.
by catnaroek 9y ago
It's an empirical fact that people use languages they couldn't have designed themselves. Designing a safe language requires mathematical sophistication. Using a safe language - less so. As for cowboy programming, Java and C# don&#
60.
by catnaroek 9y ago
Last time I checked, psychology doesn't affect how a computer program runs.

More ›