dis gon be good https://youtu.be/qT8NyyRgLDQ

>>8594713
>Faggot computer scientists still try to pretend they are mathematicians
>There is still no axiomatization of computer science

Lol, try again. Wildberger's axioms would actually be pretty good for the axioms of computer science so I say before you start drowning on your own cum you give him a call and start my formalizing your entire field and then you can talk about diving deeper into pure mathematics via CS.

>>8594742

I don't see the problem of using syntax checking etc to see if mistakes were made. From what I understand what he means with the proof checking is assert whether the expected outcome matches the real outcome. This would allow you to create subsets of the proofs, and identify problems faster by being able to check each set individually.

>>8594742
I see no problem whatsoever in implementing Wildbergers system in any language. Go with
"|"
"||"
"|||"
"||||"
...
as natural numbers and write functions between that do arithmetic.
That's basically what he wants.

This is actually pretty good.

>>8594713
>>8594742
About 4 years ago I first ran into type checking and ML/SML from the math department and not the CS department. CS shills will probably think ML/SML = machine learning.

>>8594713
>all this shilling for constructivist mathematics
/sci/ is a classical board, get OUT

>>8596106
What's important is you've found a way to feel superior to both departments.

>>8596123
It's actually a quite constructively oriented math "forum", in comparison to others

>actual computer science gets posted on /sci/
>it's all programmer hooey

it's almost like nobody here understands category theory ja

>>8594713
From the thumbnail I thought this was the Amazing Atheist.

>>8596123
>tfw constructivism, type theory, and category theory grow more and more popular each year

Your days are numbered setcuck