Hacker News Reader

JoeCamelon Why is dependent type theory more suitable than set theory for proof assistants?

I'm a beginner in proof assistents, can you give some examples of many kinds of math ruled out? And what is UIP?

> Why start calling things 2-vectors, when you could call them 2-forms and people would know what you were talking about?

There is more to 2-forms. Also, to be precise, they are functions from a vector space to the scalar field (usually reals). Sure, they form a (dual) vector space but I think it would be more confusing to call GA elements k-forms.

JoeCamelon Hindley-Milner Type Inference (2012)

I would argue that trying to describe our physical world and reality has only one "axiom" which is: your description has to be consistent with our observations of the world. Mathematics doesn't have this limitation so I don't think your example is valid. If you don't like LEM, fine, maybe there is something interesting in systems without LEM, but most math is done with LEM. I don't think is a matter of "right" and "wrong".

JoeCamelon Hindley-Milner Type Inference (2012)

I don't understand what "LEM is false" means. What are your starting assumptions that lead to the "LEM is false" conclusion? You can use/assume LEM in your system or not, most mathematicans assume LEM (without even thinking about it).

JoeCamelon A 2020 Vision of Linear Algebra

I also think that this point should be emphasized more. It helped me a lot when I realized it. I also liked the abstract approach to vector spaces. Of course, a matrix is just one way to represent linear transformations and it can also represent other things like a system of linear equations.

JoeCamelon Swift: Google’s Bet on Differentiable Programming

Obviously "more powerful" doesn't imply the capability of solving the halting problem. What exactly do you want to say? You are not impressed with "differentiable programming"?

JoeCamelon Rust Dataframe: Update 1

I don't have this impression. Can you explain?

JoeCamelon New Grad vs. Senior Dev

I think you are wrong. Yes, better understanding of hardware implementation (cache sizes and latency, branch prediction and pipelines, specialized instructions) is important. But also in real life those asymptotic complexities will often have similar c and N_0, or your input will be bigger than N_0, so O(n) vs O(n^2) will still matter. Basic analysis of algorithms makes your life easier because, in this simplified model, you can get a rough estimate of time/space requirements. Of course, if you have competing implementations, you will benchmark them (which is not straightforward to do properly).

By the way, usually we use "complexity theory" for a part of theoretical computer science (math) concerned with proving lower bounds (like the most famous P vs. NP). What is required for basic analysis of algorithms (without any fancy methods) is not very hard. Yes, you can search the web like we all do, but first you need to know what are you searching for. Also, we reuse algorithms/data structures but not only in the final product but also in our own new algorightms so you cannot search it.

Regarding interviews, I think the main problem is that many companies and interviewers try to blindly copy the questions (cargo cult) without understanding the point of such interviews. The point IMO is that you evaluate analytic skills of a candidate. Correct/incorrect answer is not everything. You could do the same with math, science problems but algorithms/data structures are closer to programming. Anyway, I feel this is becoming a controversial topic.

JoeCamelon It's not what programming languages do, it's what they shepherd you to

Do you have examples of languages which don't encourage you to use array of structures?

JoeCamelon Requirements volatility is the core problem of software engineering

To clarify, I use "programmer" when speaking to very non-technical people, usually elderly. Many other languages have a similar word but it might have different connotations, for example, be less negative (pejorative).

JoeCamelon Requirements volatility is the core problem of software engineering

What does the word "developer" mean to other people? If you want to keep it simple, why not "programmer"?

Depending who I talk to, I use "programmer" or "software engineer" most often.

JoeCamelon Requirements volatility is the core problem of software engineering

* "Engineering is the use of scientific principles to design and build machines, structures, and other items"

* Mathematics isn't only about calculation and applied physics. When you write a simple algorithm and convince yourself with a logical argument about its correctness, time complexity, etc. that is math too. You also do calculations when you design various systems (latency, throughput, etc.)

* I know a dozen mechanical, structural, and electrical engineers. They almost never model anything from first mathematical principles, they use well known tools and methods they learned. Their "nail guns and glue". Actually I think most of them don't understand math/physics behind it very deeply. So even if those methods are underpinned with mathematics and physics, it's abstracted away most of the time which is good for practical purposes.

Even in "user-interface programming", I often had to use math, algorithms, etc. In other parts of software engineering I used it much more.

JoeCamelon Rust: Zero-Cost Abstraction in Action

I think it's both about abstraction and compile time optimization. The point was that by default you can write code that uses higher level abstraction but compiles to the same code as an imperative-style loop. Most used languages or default implementations don't use LLVM, moreover they are interpreted or JIT compiled, so there might be different performance between e.g. for-loops vs. forEach with a closure.

JoeCamelon Rust: Zero-Cost Abstraction in Action

Usually in Rust community zero cost means zero runtime cost. Obviously, there are many other costs you could define.

JoeCamelon Projective Geometric Algebra Done Right

It seems the post is a response to SIGGRAPH 2019 course “Geometric Algebra for Computer Graphics” and not a stand-alone introduction to GA. Maybe the title suggests otherwise. That explains why there are no figures. I have a basic knowledge of GA but everything seemed clear. I was confused a little bit by "anti-scalar" which is usually called "pseudo-scalar".

JoeCamelon Public keys are not enough for SSH security

What is a modern passphrase? Or modern OpenSSH?

JoeCamelon Public keys are not enough for SSH security

How do you enforce it?

JoeCamelon Actix-web 1.0 – A small, pragmatic, and fast web framework for Rust

I've just run it and it works! I didn't know about the macro.

JoeCamelon ARM Assembly Language Using the Raspberry Pi

I teach people that there are many ways to encode numbers into 0, 1 symbols (state of switches). One obvious way for natural numbers is base-2 (with more significant bits on the left). It get's more complicated with negative numbers (two's complement usually, but could also be one sign bit). Floating point numbers are hard. You could also use variable length integers where small numbers are represented with less bits and you use one bit to mark end of a number (every 8 bits).

JoeCamelon Europe mostly ends mobile roaming fees from today

Didn't notice any price changes in Croatia. I pay ~15 EUR for unlimited calls, SMS, and mobile data (it's limited to 10 GB in roaming).

JoeCamelon Europe mostly ends mobile roaming fees from today

You should check if your unlimited plan applies to roaming. I have a unlimited data plan in Croatia, but in roaming it's limited to 10 GB.

JoeCamelon Europe mostly ends mobile roaming fees from today

There is of course fair use policy https://en.wikipedia.org/wiki/European_Union_roaming_regulat...

JoeCamelon Europe mostly ends mobile roaming fees from today

Which telcos and in which country? Everything seems fine here in Croatia.

JoeCamelon Europe mostly ends mobile roaming fees from today

No, calling foreign numbers costs the same in both your country and abroad. And it's usually more expensive on mobile networks, but that doesn't have anything to do with roaming.

JoeCamelon Does 1+2+3+... Really Equal -1/12?

I loved this video https://www.youtube.com/watch?v=XFDM1ip5HdU "An exploration of infinite sums, from convergent to divergent, including a brief introduction to the 2-adic metric, all themed on that cycle between discovery and invention in math."

JoeCamelon Fujifilm's new X-T2 camera has 24 megapixels, 4K video, and great controls

They probably forgot to mention because all Fuji X-series mirrorless cameras are APS-C. There is also a rumor that Fuji will release medium format mirrorless cameras soon...

JoeCamelon Seldomly Used SQL: The Bool Aggregate Functions

Why "JOIN foo USING (bar)" shouldn't be used?

JoeCamelon Show HN: React-Designer – Editable Vector Graphics in React Components

What do you mean by "reflectDOM method"? Can you explain a little bit how will you deal with this? I've searched the repo but couldn't find anything regarding reflect. Thanks!

JoeCamelon Show HN: An IDE for poets

  your thoughts never reference me
  i should be marked-and-swept
  but there is nobody to collect me
  i am a soul leak

JoeCamelon Nikola Tesla Wasn't God And Thomas Edison Wasn't The Devil

Maybe this awesome illustration by Travis Pitts gives a good picture of how people see Tesla http://www.flickr.com/photos/zom-bot/7227505456/sizes/o/in/p... :)