JoeCamel

I don't read it like that at all. Rust is mentioned only once. Nevertheless I do care if a tool I am considering to use is written in JavaScript, Rust or some esoteric language. It means a lot, not only for "safety" which is not important to you that much, but also for maintainability, community, and the future of the project. Of course, what triggers you probably is mentioning Rust in the title of the post. Still hard to imagine being so annoyed by it–if authors thinks it's important or it will grab attention, why not use it...

Saying Lean "rules out many kinds of mathematics" and not giving a single example, sounds more sensationalist to me. I also don't see what's wrong with anonymous comments as long as they are constructive and people are nice.

I don't know Kevin as well as you do (apparently) but maybe he is just ignorant on the topics you know so much about. Why something gets attention of media (Quanta Magazine?) is complicated. From your comments, you also seem very "bold".

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.

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".

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).

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.

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"?

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

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.

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

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).

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.

* "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.