Program GOTO to jedno z narzędzi teorii obliczalności służące do ustanowienia, czy dana funkcja jest obliczalna.
Cechy Klasa funkcji obliczalnych za pomocą GOTO odpowiada klasie funkcji obliczalnych za pomocą maszyny Turinga lub programów WHILE. Program GOTO, podobnie jak program WHILE, może popaść w pętlę nieskończoną. Za pomocą programu GOTO dają się przedstawić zarówno funkcje totalne, jak również funkcje częściowe.
Formalna definicja Składnia Programy GOTO składają się z symboli: GOTO, IF, THEN, HALT, Mi, =, +, -, :, ;, := oraz dowolnej liczby zmiennych i stałych.
Program P jest syntaktycznie zdefiniowany w notacji BNF jako:
Instrukcja I jest zdefiniowana jako:
gdzie: jest stałą, elementem zbioru liczb naturalnych są zmiennymi jest znacznikiem to instrukcja stopu
Semantyka Wszystkie użyte w danym programie zmienne zostają zainicjalizowane przed wykonaniem programu.