История изменений

В дополнение: по Clojure/Clojurescript есть вакансии, обычно за них хорошо платят. Если ты джавист/фронтендщик, тебе это вполне может помочь. Лисп лечит (ну или калечит, смотря к кому он применён). А вот я посчитал в Z3, сколько будет 2+2. Это не лисп-система, а система доказательства теорем, поэтому так сложно.

$ z3 -smt2 -in
(declare-fun x () Int) ; хз что это значит, ChatGPT набредил
(assert (= (+ 2 2) x)) ; добавляем в теорию уравнение 2 + 2 = x
(check-sat) ; решаем нашу теорию
sat ; z3 нам сказал, что есть решение
(get-value (x)) ; извлекаем, чему же равен x в этом решении
((x 4))

В дополнение: по Clojure/Clojurescript есть вакансии, обычно за них хорошо платят. Если ты джавист/фронтендщик, тебе это вполне может помочь. Лисп лечит (ну или калечит, смотря к кому он применён). А вот я посчитал в Z3, сколько будет 2+2. Это не лисп-система, а система доказательства теорем, поэтому так сложно.

$ z3 -smt2 -in
(declare-fun x () Int)
(assert (= (+ 2 2) x))
(check-sat)
sat
(get-value (x))
((x 4))