Coronal mass traveling at a higher speed "sweeps" what's before it. You can see the spiral shape, and you can probably figure out that the stuff is slowing down as it moves outward.
Watch this occasionally for a few months and you'll get the idea, although solar activity is slowing down somewhat (as expected).
If you carefully re-read what GP wrote, you'll see there's no reference to Earth's orbit or 1 AU in there. GP wrote about the solar wind scattering cosmic rays when it reached some point in its outward travel.
I think so! You can codegen Ocaml directly, which means you have the benefit of lots of nice compiler libs and tools right out of the gate, but the metatheory is also expressive enough that your source language can be pretty wild with your denotational semantics. Grain of salt though, because I haven’t tried this concept in anger at all
personally i think you should just have a separate proof language that doesn't also try to be a programming language and build a bridge between them (ideally as a compilation target). anyways im working on this with my spare opus tokens.
What do you mean by this? I don’t want to be annoying and throw “propositions-as-types” at you, but as I understand it, F* is very much already doing this.
Its type system is the proof language/metatheory for making propositions, and its programs are their proofs, and there’s an intermediate form, core F*, that we elaborate to, a partial evaluation phase where we actually use the dependent types to simplify our AST, then codegen/lowering. In your analogy, I would call their core IR the bridge I guess? To clarify, I’m not trying to be a dick, I’m trying to sus out if I’ve understood you correctly
They started out that way. Keeping consistency between the formal specification and the code was always difficult. The further apart they are in distance or notation, the more difficult it is. So, the field experimented with verificatiom-oriented languages to localize changes.
reply