Distinguish math symbols in the language and the meta-language

It might not be quite the official interface but you can reset to the normal font regime with fam=-1

\documentclass{article}
\usepackage{xcolor}

\definecolor{string}{Hsb}{330,0.8,1}
\definecolor{meta-string}{Hsb}{330,0.8,0.6}
\def\formal#1{\mathsf{\color{string}#1}}
\def\meta#1{\begingroup\fam-1 \color{meta-string}#1\endgroup}

\newcommand\lthen{\rightarrow}

\begin{document}

$\textcolor{string}{\mathsf{p} \lthen (\textcolor{meta-string}{F_1} \lthen \mathsf{p})}$

$\formal{p \lthen (\meta{F_1} \lthen p)}$
\end{document}

This is a rather slow (but not so much it becomes really noticeable) implementation of your last idea:

\documentclass{article}
\usepackage{amsmath,sansmath,xcolor}
\definecolor{string}{Hsb}{330,0.8,1}
\definecolor{meta-string}{Hsb}{330,0.8,0.6}
\newcommand\lthen{\rightarrow}

\makeatletter
\def\change@code@lc#1\relax{%
  \mathcode#1=\string"8000
  \begingroup\lccode`~=#1
  \lowercase{\endgroup\def~}{\text{\normalfont\sffamily\char#1}}%
}
\def\change@code@uc#1\relax{%
  \mathcode#1=\string"8000
  \begingroup\lccode`~=#1
  \lowercase{\endgroup\def~}{%
    \text{\normalfont\sffamily\slshape\color{meta-string}\char#1}%
    \@ifnextchar_\@uc@subscript{}}%
}
\def\@uc@subscript_#1{_\text{\color{meta-string}$#1$}}

\protected\def\formal{%
  \hbox\bgroup
  \count@=\numexpr`a-1\relax
  \loop\ifnum`z>\count@
  \advance\count@\@ne
  \expandafter\change@code@lc\number\count@\relax
  \repeat
  \count@=\numexpr`A-1\relax
  \loop\ifnum`Z>\count@
  \advance\count@\@ne
  \expandafter\change@code@uc\number\count@\relax
  \repeat
  \@formal
}
\def\@formal#1{\sansmath\color{string}$#1$\egroup}
\makeatother

\begin{document}
\formal{p \lthen (F_1 \lthen p)}

\begin{align}
&\formal{A\lthen b}\\
&\formal{C\lthen D}
\end{align}
\end{document}

The align is just to show that it works (to a limited extent) also in alignments: the argument to \formal cannot contain a & for the alignment.

Regarding your last idea:

It is not very difficult to use for certain symbols/letter another font. E.g. here for the p:

\documentclass{article}
\usepackage{xcolor}
\newcommand\lthen{\rightarrow}
\DeclareSymbolFont{formalletters}{OT1}{cmss}{m}{n}
\DeclareMathSymbol{p}\mathalpha{formalletters}{"70}
\begin{document}
$p \lthen (F_1 \lthen p)$
\end{document}

But it is difficult to add colors in this case.

This is easier with xelatex/lualatex as there you can add color directly to the font:

\documentclass{article}
\usepackage{xcolor}
\usepackage{unicode-math}
\setmathfont[Color=00FF00]{lmodern-math.otf}
\ExplSyntaxOn
%\bool_set_true:N  \g_um_uplatin_bool %for upright p
\ExplSyntaxOff
\setmathfont[range={"61-"7A, %a-z
                    "02192, %\rightarrow
                    "00028-"00029% parentesis
                    },
             Color=FF0000]{lmodern-math.otf}
\newcommand\lthen{\rightarrow}
\begin{document}
$p  \lthen (F_1 \lthen p)$

\end{document}

(The name for the lm modern math font can differ on your system). If you need beside your "formal math" also normal math you can (probably as I didn't test) set up a \mathversion for the "formal math".