Hacker News new | ask | show | jobs
by lwerdna 1562 days ago
- How type theory can prove mathematical theorems. I can limp through the first exercises of Software Foundations, but eventually realize I'm just "making it work" instead of knowing how it works. Only made it halfway through My Little Typer and even implemented STLC and used it to prove simple propositions with implications. But I still couldn't tell you how dependent types magically make it possible to prove real theorems.

- How opamps work and how they're used to make a differentiator.

- How quantum computing works. I want understand it to understand why factoring and discrete log fall to QC but not the post-quantum algorithms. I never make it past the intro chapters.

- What exactly makes cryptographic hash functions have desirable properties like collision resistance? Bits go in, bits go out, why can't full observation of the process not yield a method to construct inputs for a target output? Similar questions for block ciphers. It is much easier to "see" the impossibility in public key schemes because you can play and experiment with the math. In symmetric algorithms it looks like just a bunch of arbitrary bit operations.

EDIT:

- Relativity. I accept things like time dialation and nothing can go faster than the speed of light. But I have no idea why you would experience less time passing than me after a high speed rocket trip when, from your perspective, you saw me on a high speed planet trip. Or what prevents a rocket in space with 3m/s^2 acceleration from reaching the speed of light after 100,000,000 seconds.

2 comments

>How opamps work and how they're used to make a differentiator.

An op-amp is just a very high gain amplifier. It senses the difference in signal levels and just amplifies that difference by a large amount, usually between 1000 and 10,000,000 times.

The first op-amp circuit you usually use is a negative feedback linear amplifier. In this circuit, the positive input to the op-amp is simply grounded. The input voltage is put through a resistor R1 into the negative (AKA inverting) input. The resistor limits the current into the negative input to Vin/R. As soon as the voltage on the input becomes non-zero, the output of the op amp becomes a quite large signal, of the opposite sign. If you feed a small amount of that signal back to the same negative input, (through a feedback resistor R2) the signal will rise until the feedback current balances out the input current.

Now it's not exactly in balance, as there is a very small deviation that has to drive the amplifier to keep its output up, but for most uses the higher the gain of the amplifier, the lower that deviation has to be.

This circuit has a gain of -R2/R1

If you replace the input resistor in the above circuit with a capacitor. It will pass a current proportional to the change in voltage/time and the capacitance. If you feed in a steadily rising voltage, you'll get a current into the negative input of the amplifier that is proportional to the derivative of the input voltage, the feedback current will balance this out, and you'll thus end up with a scaled up derivative of the input.

This circuit has a gain of dv/dt * -R2/(1/c)

If you start with the first circuit and replace the feedback resistor with a capacitor, you'll find that the output has to rise at a rate proportional to the input voltage to balance the input, making an integrator. This only works up to the limit of the output voltage, and there may be a small amount of uncorrected input bias.. to counteract this, a large resistance will be placed in parallel to the capacitor, to keep the output from becoming pegged with no input.

This circuit has a gain of -Integral(Vin)* (1/C) / R1

Notice in all of these equations, the gain is the ratio of the -feedback impedance/input impedance

Does that make sense?

I think a better way to go through the exercise is to remember the principles of an ideal op amp: The inputs have infinite input impedance and zero voltage drop across them.

You can derive the behavior of op amp building blocks from these rules and Kirchoff's laws. It also makes things obvious, like ideal vs practical integration.

That works for people who just trust formulae, but for those of use with a background in breadboards and solder, the real world behavior of op amps isn't perfect, and we need to understand it in terms of what we already know.

I'm going through the same learning curve with quantum gates. Nobody shows the physical layout of the devices involved, signals going through them, etc.

Ultimately an op amp is a hardware abstraction. Often you teach the abstraction first through its interface to understand how it allows building useful things. Then you can teach the implementation behind that interface, and all the design trade offs. And just like the formulae, you need to understand that it's a tool for simplification - distrust shouldn't come into play, just proper understanding.

At least in my EE undergrad we were taught why you would want an op amp before we were taught how to design multi stage amplifiers with discrete transistors. In fact most of the real world limitations of op amps don't require knowledge of what's going on under the hood, least of all the physical layout of the chip. Even a schematic diagram of the simplified model for a UA741 is more than you'd ever need except for a shitty SPICE emulation.

I empathize with what you're getting at, but I've seen that mentality turn into the bane of practical or working knowledge of many technical topics. It is a skill to be able to learn just what you need to learn and decide what level of detail is enough, and most of the time that skill is only provided through instruction and mentorship.

As an addendum, I'd add that Sedra and Smith wrote an amazing textbook on semiconductors that I highly recommend anyone interested in the topic should read. Here's an Amazon link to the book: https://www.amazon.com/Microelectronic-Circuits-Electrical-C...
Here's a good introduction to Special Relativity, which is what you asked about:

http://www.av8n.com/physics/spacetime-welcome.htm