top | item 29727140

(no title)

liups | 4 years ago

> pure math (topology and countability) and computer science have almost no overlap in the short term.

This is an unexpected opinion. What do you mean by this?

I would argue the opposite.

Look at Formal Verification[0].

Here's a great video about a popular formal verfication proof assitant: https://www.youtube.com/watch?v=Dp-mQ3HxgDE

A quote from the mathematician in the video expressing enthusiasm for using computers for mathematics: "All I want to do... I don't want to do mathematics on pen and paper anymore, because I don't trust it, and I don't trust other people that use it; which is everyone." (in case people only read this quote, instead of watching the lecture, the tone is tongue-in-cheek)

Formal Verification would seem a literal intersection of pure math (formal proofs[1]) and computer science (formal specification[2]).

Of note, one of the popular underlying foundations of an approach to formal verification is Homotopy Type Theory(HoTT)[3][4] which is an asserted effort to show the relationship between type theory and, specifically, topology (homotopy[5]).

[0] https://en.wikipedia.org/wiki/Formal_verification : fancy word for 'computer verified mathematical proofs'

[1] https://en.wikipedia.org/wiki/Formal_proof : fancy word for 'proof'

[2] https://en.wikipedia.org/wiki/Formal_specification : fancy word for 'rules for an algo that checks a proof'

[3] https://en.wikipedia.org/wiki/Homotopy_type_theory

[4] https://homotopytypetheory.org/book/ : a great read, even if you are a novice, or prefer other formal verification foundations

[5] https://en.wikipedia.org/wiki/Homotopy_theory : "It originated as a topic in algebraic topology"

discuss

order

No comments yet.