what difference between propositions and `if` statement of program Consider a proposition,
$$\forall x\in\mathbb{R}~(x^2<0\implies x=23)\tag{1}$$
Due to vacuous truth, Obviously it's a true proposition, However I have confused by it when transform this proposition to a program. Such as:
if(x² < 0){
  return 23;
}

We know the statement will never be executed, because x² always greater or equal than zero, I don't know, Does a mathematics proposition can be transformed to if statement in program, if my transformation is wrong, how to transform this proposition?
TABLE
A   B   T/F
___________
T | T | T
T | F | F
F | T | T
F | F | T

 A: You are confusing two uses of the combination  "if.....then".  In math it is a connective, a way of linking two sentences into one sentence.  We define that in "if A then B" if A is false the compound sentence is true.  In programming "if A then B" means "if A is true, do B, and if A is false do not do B".  These are not at all the same.
Programming languages like FORTRAN and Python also have a completely different meaning for the equals sign.  It is normal to write $I=I+1$ except in Python you use lower case.  The equals sign is not what mathematicians use it for, it is a direction to compute the right hand side and store that in the address indicated by the left hand side.  The left side has to be essentially a single variable.
In English, whether you consider "if A then B" to be true when A is false is ambiguous.  If I say "If 2+2=5 then the moon is made of green cheese." is that true, false, or nonsense?  I think most people would opt for nonsense.  In English "if ..... then" has a sense of the first causing the second.  In math it is clearly true.
Meanings change due to context.
A: The material implication symbol $\implies$ (which is sometimes called the "if" symbol) is pretty much totally unrelated to if-statements in computer programming.
In classical logic (the kind of logic that mathematicians use 95% of the time, perhaps), the statement $p \implies q$ is simply an abbreviation of $(\neg p) \lor q$. It means exactly that, no more, no less.
So, the correct way to translate $x^2 < 0 \implies x = 23$ into computer code would be something like this:
function my_predicate(x) {
    let p = (x² < 0);
    let q = (x == 23);
    return ((!p) || q);
}

Then the sentence $\forall x\in\mathbb{R}~(x^2<0\implies x=23)$ is equivalent to the assertion that the function my_predicate is equivalent to the function always_true, as defined like so:
function always_true(x) {
    return true;
}

