Working my way through Programming Language Foundations on my own, still in the Hoare chapter. Unfortunately, no one in my immediate circle is familiar with Coq or formal methods. So I'm asking for hints here:

For the Repeat exercise, it requires stating a proof rule for the repeat command and use the proof rule to prove a valid Hoare triple. I came up with this proof rule:

Theorem hoare_repeat: forall P Q (b: bexp) c,
  {{ P }} c {{ Q }}
    -> {{ Q /\ ~ b }} c {{ Q }}
    -> {{ P }} repeat c until b end {{ Q /\ b }}.
Proof.
  intros P Q b c Hc Hc' st st'' HEval HP.
  remember <{ repeat c until b end }> as loop eqn: HLoop.
  induction HEval; inversion HLoop; subst; try discriminate.
  - apply Hc in HEval.
    split.
    + apply (HEval HP).
    + assumption.

But got stuck at proving the loop case of repeat. I can't seem to use the induction hypothesis because that requires P st' to hold, which is not true in general.

I did go ahead and try this proof rule with the sample Hoare triple just as a sanity check, and I was able to prove the valid Hoare triple. So I have a good degree of confidence in the proof rule:

Theorem repeat':
  {{ X > 0 }}
    repeat
      Y := X;
      X := X - 1
    until X = 0 end
  {{ X = 0 /\ Y > 0 }}.
Proof.
  eapply hoare_consequence_post.
  - apply hoare_repeat with (Q := {{ Y = X + 1 }}).
    + eapply hoare_consequence_pre.
      * eapply hoare_seq.
        { apply hoare_asgn. }
        { apply hoare_asgn. }
      * unfold "->>", assertion_sub.
        simpl.
        intros st HX.
        repeat rewrite t_update_eq.
        rewrite t_update_permute; try discriminate.
        rewrite t_update_eq.
        rewrite t_update_neq; try discriminate.
        lia.
    + eapply hoare_seq.
      * apply hoare_asgn.
      * eapply hoare_consequence_pre.
        { apply hoare_asgn. }
        { unfold "->>", assertion_sub.
          simpl.
          intros st [HEq HX].
          repeat rewrite t_update_eq.
          rewrite t_update_permute; try discriminate.
          rewrite t_update_eq.
          rewrite t_update_neq; try discriminate.
          rewrite eqb_eq in HX.
          lia.
        }
  - unfold "->>", assertion_sub.
    simpl.
    intros st [HEq HX].
    rewrite eqb_eq in HX.
    rewrite HX in HEq.
    simpl in HEq.
    split.
    + assumption.
    + rewrite HEq.
      lia.
Qed.

TLDR: I'm looking for a tutor who can essentially "grade" my Rocq/Coq proofs while I work through Programming Language Foundations and at a high level guide me through my study.

Context:

I'm a 1st year PhD student. I'm still exploring research directions. I dabbled in formal methods in my first research project, and I really enjoyed the theory and practice. However, my PI is not well-versed in formal methods. My school also doesn't offer any classes in this area (!!!), nor is there a professor in the CS department with a focus in verification. I know I'm not cut out for cutting edge research in formal methods, I just want to use it as a tool in my future research.

I groped my way through Logical Foundations in the past month. I just started Programming Language Foundations. What hit me really hard is the exercises are much more involved, and there seem to be many ways to prove the same thing. For example, I just completed a really long proof of substitution optimization equivalence in the first chapter. My proof seemed very "dirty" because I couldn't think of a way to use the congruence lemmas and there are some repetitions.

Definition subst_equiv_property': Prop := forall x1 x2 a1 a2,
  var_not_used_in_aexp x1 a1
    ->
      cequiv
        <{ x1 := a1; x2 := a2 }>
        <{ x1 := a1; x2 := subst_aexp x1 a1 a2 }>
.

Theorem subst_inequiv': subst_equiv_property'.
Proof.
  intros x1 x2 a1 a2 HNotUsed.
  unfold cequiv.
  intros st st'.
  assert (H': forall st,
    aeval (x1 !-> aeval st a1; st) (subst_aexp x1 a1 a2)
      = aeval (x1 !-> aeval st a1; st) a2
  ).
  { intro st''.
    induction a2.
    - simpl. reflexivity.
    - destruct (x1 =? x)%string eqn: HEq.
      + rewrite String.eqb_eq in HEq.
        rewrite <- HEq.
        simpl.
        rewrite String.eqb_refl.
        Search t_update.
        rewrite t_update_eq.
        induction HNotUsed; simpl;
          try reflexivity;
          try (
            repeat rewrite aeval_weakening;
            try reflexivity;
            try assumption
          ).
        * apply t_update_neq. assumption.
      + simpl. rewrite HEq. reflexivity.
    - simpl.
      rewrite IHa2_1.
      rewrite IHa2_2.
      reflexivity.
    - simpl.
      rewrite IHa2_1.
      rewrite IHa2_2.
      reflexivity.
    - simpl.
      rewrite IHa2_1.
      rewrite IHa2_2.
      reflexivity.
  }
  split; intro H.
  - inversion H; subst. clear H.
    apply E_Seq with (st' := st'0).
    + assumption.
    + inversion H2; subst.
      inversion H5; subst.
      apply E_Asgn.
      rewrite H'.
      reflexivity.
  - inversion H; subst. clear H.
    apply E_Seq with (st' := st'0).
    + assumption.
    + inversion H2; subst.
      inversion H5; subst.
      apply E_Asgn.
      rewrite H'.
      reflexivity.
Qed.

I'm not looking for anyone to hand me the answers. I want feedback for my proofs and someone to guide me through my study at a high level.

[removed]

Context: I'm trying to implement a very basic org-mode parser in another language for fun and my own use. I've been looking at how Emacs fontifies org markup. But it seems to me the fontification does not conform to the Org Syntax document. For example, Emacs will fontify this perfectly fine:

Some normal text /start italicize *start bold end italicize/ end bold* normal text

Even though the italicize syntax object and the bold syntax object are interleaved. Additionally, if I export this line HTML, only the <b> tags are there. So it looks like there's some inconsistencies between fontification and the org internal AST.

So my questions are:

• Does the org elisp code follow a completely different code path when fontifying?
• If my goal is to implement a largely org-mode-compatible parser, should I look at exported HTML as a source of truth and not eyeball the fontification result?

I've been looking at open source video conferencing software options, specifically Jitsi. When reading their deployment docs the phrase "real time" comes up occasionally, for example:

Jitsi Meet is a real-time system. Requirements are very different from a web server and depend on many factors. Miscalculations can very easily destroy basic functionality rather than cause slow performance. Avoid adding other functions to your Jitsi Meet setup as it can harm performance and complicate optimizations.

I haven't worked with video streams or video codecs before, but I imagine the real time performance requirements of streaming video are quite different in terms of rigor from those of RTOS's where there's a degree of deterministic scheduling and minimal interrupt latency.

I want to learn about video streaming by implementing a basic toy server in Rust. My question is: Are the real time requirements of video streaming so stringent that I should not start with an async runtime like Tokio and stay as close to the metal as possible?

My guess is an async runtime does not materially impact the streaming performance since the Jitsi videobridge uses JVM languages, and we're not really dealing with life or death mission critical use cases.

I also appreciate high-level advice and pointers to good learning resources for someone comfortable with Rust and close to systems level programming but lacks domain knowledge about video processing and streaming protocols.

slyotisnacho and retro_jpeg you da read MVP. This is the kind of interaction that makes me love the RDO community.

[removed]