Dependent types were created to deepen the connection between programming and logic.
依存型は、プログラミングと論理学のつながりを深めるために作られた。