Так кроме афинной есть еще линейная логика например в Linear Haskell, другое дело, что обычно это все ортогонально производительности и массовому программированию. Конечно, выглядит перспективным писать доказательства вместо программ или программы вместе с доказательством ( типа Idris с Agda ), но по факту если программа без доказательства приносит деньги, деньги будут вкладываться в такие программы. Вообще говоря, типизированные программы и есть частично такие доказательства, которые пишутся вместе с программами, но даже тут кода на нетипизированных языках написано гораздо больше ( согласен что ламерами ), но машинка крутится и конца пока не видно.