In programming languages, generally we do not distinguish relations and functions. Is there a better way to deal with these two concepts?
Let $A$ be any set. Then, its powerset $\mathcal{P}(A)$ is isomorphic to the function space $A\to \mathbb{B}$ where $\mathbb{B}=\{\sf true, false\}$.

Indeed, the isomorphism is given by mapping each subset to its own characteristic function.

$$
\begin{array}{lcl}
\mathcal P A &amp; \leftrightarrow &amp; (A \to \mathbb B) \\
X &amp; \mapsto &amp; \lambda a. {\sf if}\ a\in X\ {\sf then\ true\ else\ false} \\
\{a|g(a)={\sf true}\} &amp; \leftarrow\!\shortmid &amp; g
\end{array}
$$

Since relations are sets of pairs, relations too can be seen as binary functions whose codomain is $\mathbb B$.

In most programming languages, as you realized, we don't really find propositions, sets, or relations, but we instead find their isomorphic counterparts: booleans, unary boolean functions, binary (or more) boolean functions.

This choice is mostly suggested by the fact that everything we compute ultimately is represented by a few bits. It is therefore very efficient for a computer to represent the truth values associated to propositions. Further, it is convenient to be able to write e.g. b = b or (y &lt; 5) without using a conditional. (Actually, using a conditional for that usually reveals that the programmer does not understand that boolean expressions are indeed expressions, and not special syntax that is relegated to conditional or loop guards. This phenomenon also shows up in the infamous if b==true ... where the programmer often thought that we have to use at least one boolean operator in the guard, since we usually need that.)

In programming languages, there are some theoretical contexts where we do separate propositions from booleans, though. For instance, in the calculus of inductive constructions, as implemented in Coq, we find a Prop type for propositions, and a bool type for booleans. Very roughly, this allows the programmer to deal with propositions that can not be automatically checked by the computer, e.g. $\forall a,b,c\in\mathbb N.\ (a+b)\cdot c = a\cdot c + b\cdot c$
is a Prop. Even if the computer can not check them, we can still mathematically prove them. Note that we can not turn a Prop into its bool truth value since we have no way to check $\forall n$ or $\exists n$. (Actually, there's no such a thing as its "truth value" since the logic is constructive, but I'll be silent about this.) By comparison, we get two forms of n &lt; 4 comparisons: one which is a Prop and can be used in logic, and another one which is a bool and can be used in programs.