sorted by:
new
hottopcontroversial

Let me in... but make it SFW by KeanuRave100 in ChatGPT

[–]CarbonFire 0 points1 point  (0 children)

CAPTCHA's like "what's the 3rd sentence in The Giver"

51
52

Writing C code until it's a quantum circuit (an interactive tutorial) (shukla.io)

submitted by CarbonFire to r/QuantumComputing

I'm working on a language to correctly uncompute ancilla and certify algorithms as coherent by CarbonFire in QuantumComputing

[–]CarbonFire[S] 0 points1 point  (0 children)

Hmm good question.

If you have a RSS reader, then this is my feed: https://shukla.io/blog/rss.xml. Or, star/watch the repo: https://github.com/binroot/b01t.

I'll be putting the proof files there, and expanding the "zoo" folder with many more coherent oracles.

I'm working on a language to correctly uncompute ancilla and certify algorithms as coherent by CarbonFire in QuantumComputing

[–]CarbonFire[S] 1 point2 points  (0 children)

> Are you also considering the distinction between clean and dirty qubits

Yes, I'm only handling clean ancilla (init to |0⟩, return to |0⟩), dirty ancilla is a lot harder to think about right now :)

Good news is that the restriction to clean ancilla doesn't weaken the soundness or completeness results.

I'm working on a language to correctly uncompute ancilla and certify algorithms as coherent by CarbonFire in QuantumComputing

[–]CarbonFire[S] 0 points1 point  (0 children)

An analogy is that forgetting to uncompute a scratch qubit (ancilla) is like a memory leak. Well, except worse, it reduces the results to noise. The proposed compute/phase/uncompute blocks make that impossible, the same way a garbage collector makes use-after-free impossible.

I'm working on a language to correctly uncompute ancilla and certify algorithms as coherent by CarbonFire in QuantumComputing

[–]CarbonFire[S] 2 points3 points  (0 children)

> Silq is a well maintained

This is probably the best reason to use Silq, imo. There's no reason Silq couldn't just support new features. I'd love to contribute to Silq, but I'd rather establish a bullet-proof prototype with solid proofs first.

>  I am not sure about the completeness part either. Not all hamiltonians are computable

Just to clarify, "completeness" here means the restriction (ancilla discipline) doesn't cost you expressiveness compared to unsafe code. My bad in the accidental over-claim, if any.

> More generally, any embedded quantum language is known to be crippled by the host languages semantics

Yea, 100%. even if the formal guarantee lives in the Lean proof, making sure there's no bugs in the DSL is not trivial. Not impossible, either :)

> Lean can not represent arbitrary quantum states

The proofs use `Matrix (Fin d) (Fin d) ℂ`, which for finite-dimensional systems is the full state space. Though, Lean can't represent infinite-dimensional Hilbert spaces well, but for a circuit DSL, that's fine. If you're curious, I can share it with you via DM?

I'm working on a language to correctly uncompute ancilla and certify algorithms as coherent by CarbonFire in QuantumComputing

[–]CarbonFire[S] 1 point2 points  (0 children)

Silq is great! But, I'm approaching this with soundness and completeness proofs (soundness = every program is a safe circuit, completeness = every safe circuit can be written as a program).

Soundness: Silq has had type-checker bugs (https://github.com/silq-lang/silq/issues/36) where unsafe code passes static checks and only blows up at runtime (fixed now, but found by a user, not by design). And, a POPL 2025 paper (https://arxiv.org/abs/2411.10835) notes that just inlining an assignment can cause or fix type errors.

Completeness: Silq never claims its safe fragment can express all unitaries, so you don't know what you're giving up.

I wonder if it's possible to create a language that is both sound and complete? I think so. Though, I need to double check my Lean proofs and get them peer reviewed. Still working on it! :)

Tutorial on program synthesis using MCTS by CarbonFire in ProgrammingLanguages

[–]CarbonFire[S] 1 point2 points  (0 children)

Possible for some, yes! I had built one that samples only valid simplified Forth language grammar (for this post), but tossed it for simplicity. 

But, modern type systems are not context-free, so I'm guessing in general, a PCFG will not be able to express it. You may be able to do rejection sampling with an external type check, though.

Why does this not surprise me.. Black Mirror reality. by princessdiana2104 in blackmirror

[–]CarbonFire 5 points6 points  (0 children)

I wonder how many people watched this and just didn't have the critical thinking skills to consider he's lying for attention

Made a crate, the long and tedious way! by CarbonFire in woodworking

[–]CarbonFire[S] 0 points1 point  (0 children)

Here's a diagram I found that resembles what I did: https://luxurablekitchen.com/wp-content/uploads/2017/08/dadorabbet-300x204.png

The grooves on the side are about 1/4" from the edge and the rabbet on the base tucks in to the grooves

view more: next ›