Comment by 7373737373

My favorite minimalistic example of the Metamath base language (which higher level languages can compile down to), which, saved as, say, prop.mm can be verified with the verifier:

  $c  wff  $.        $( we use this $constant as a type of formula (well formed formula) $)
  $c  ( ) ! ->  $.   $( brackets, negation, implication $)

  $v  A B C  $.      $( $variables to be used in formulas $)

  wa  $f  wff A  $.  $( $floating hypothesis "wa" which says, that A is a well-formed formula $)
  wb  $f  wff B  $.
  wc  $f  wff C  $.

  $( The following assertions define the rules to create formulas $)
  $( In Metamath (unlike Metamath Zero), definitions also use the $axiom statement type $)
  wng  $a wff ! A $.           $( "not A is a well-formed-formula" - mandatory hypotheses are (wa) $)
  wim  $a wff ( A -> B ) $.    $( "A implies B is a well-formed-formula" - mandatory hypotheses are (wa, wb) $)

  $c  |-  $.         $( this $constant will be used as a type of provable formula  $)

  $( Schemes of $axioms of propositional logic $)
  a1  $a |- ( A -> ( B -> A ) ) $.
  a2  $a |- (    ( A -> ( B -> C ) )   ->    ( ( A -> B ) -> ( A -> C ) )    ) $.
  a3  $a |- ( ( ! A -> ! B )  ->  ( B -> A ) ) $.  

  $( Definition of the Modus Ponens rule of inference in new scope; otherwise $essential hypotheses (inputs) mp1, mp2 will become mandatory for all upcoming assertions $)
  ${
      mp1 $e |- A $.                
      mp2 $e |- ( A -> B ) $.
      mp  $a |- B $.               $( mandatory hypotheses of "mp" are (wa, wb, mp1, mp2) $)
  $}

  $( A $proof states the string of symbols to be proven, followed by a list of labels used by the stack machine $)
  $( $floating and $essential hypotheses are pushed onto the top of the stack, $axioms and $proofs transform it by using the top of the stack as inputs $)
  $( When the stack is empty at the end, the proof is successful, and the proved statement can be reused in further proofs using its label $)

  $( " A implies ( B implies C) is a well-formed-formula" $)
  formula1 $p  wff ( A -> ( B -> C ) )  $= wa wb wc wim wim $.

  $( "( A -> A ) -> ( A -> A ) is true (follows from the axioms)" $)
  formula2 $p  |- ( ( A -> A ) -> ( A -> A ) )  $= wa wa wa wim wim    
                                                   wa wa wim wa wa wim  wim  
                                                   wa wa a1    
                                                   wa wa wa a2    
                                                   mp  $.