←back to thread

Parse, Don't Validate (2019)

(lexi-lambda.github.io)
389 points melse | 3 comments | 26 Jun 21 07:23 UTC | HN request time: 0.661s | source
Show context
ukj ◴[26 Jun 21 07:47 UTC] No.27639995[source]▶
Software Engineers: Parse, don't validate.

Mathematicians: Parsing is validation

https://gallais.github.io/pdf/draft_sigbovik21.pdf

replies(3): >>27640078 #>>27640121 #>>27640235 #
Drup ◴[26 Jun 21 08:41 UTC] No.27640235[source]▶
To everyone in this subthread: sigbovik is a conference published every 1st of April.

This paper is an April's fool joke. I didn't think people could take that one seriously. I guess it's a good April's fool then. :)

replies(2): >>27640542 #>>27640741 #
1. ukj ◴[26 Jun 21 10:29 UTC] No.27640741[source]▶
The conference is indeed a spoof, but in so far as what Mathematicians call a "proof" - the paper contains one. Agda is a proof assistant in the spirit of the Calculus of Constructions ( https://en.wikipedia.org/wiki/Calculus_of_constructions ).

So is the joke on Computer Scientists or Mathematicians? You decide ;)

Beware of bugs in the above code; I have only proved it correct, not tried it --Donald Knuth

replies(1): >>27641293 #
2. Drup ◴[26 Jun 21 12:31 UTC] No.27641293[source]▶
Sigbovik's jokes are of the kind where the premise is completely bonkers. The rest of the development is made with the utmost rigor to highlight said bonkersitude, Reductio ad absurdum.
replies(1): >>27641314 #
3. ukj ◴[26 Jun 21 12:34 UTC] No.27641314[source]▶
Yeah, but that is precisely how inductive types work.

"Bonkers" premises. Iterate, iterate, iterate. "Bonkers" conclusions. GIGO.

And yet the result is reified, exists and speaks for itself. So what is so "absurd" and "bonkers" about a result that is right before your eyes?

https://en.wikipedia.org/wiki/Reification_(computer_science)