Re:Dependent Types for F#
by hinkley on Tuesday December 05, 2017 @04:53PM
(#15856373)
There really does seem to be a Last Mile problem with a lot of these systems for formalism.
You're going to get garbage data from paying customers. With a good information architecture you'll have 'lines' in the system and all of the data that goes past a certain point is guaranteed to be sanitized, at which point all this formalism helps you avoid really bad mistakes.
What ends up happening most times is a set of proprietary bespoke thunking layers that progressively sanitize the data until its usable. Everybody writes their own and they either suck or took lots of effort to get right. Or, the entire system is full of uncertainty and reads like a Choose Your Own Adventure as written by a squirrel.
Maybe there's a space there between the user and the formal type system that needs a set of transformation tools. Like htmltidy, but without the html.
You're going to get garbage data from paying customers. With a good information architecture you'll have 'lines' in the system and all of the data that goes past a certain point is guaranteed to be sanitized, at which point all this formalism helps you avoid really bad mistakes.
What ends up happening most times is a set of proprietary bespoke thunking layers that progressively sanitize the data until its usable. Everybody writes their own and they either suck or took lots of effort to get right. Or, the entire system is full of uncertainty and reads like a Choose Your Own Adventure as written by a squirrel.
Maybe there's a space there between the user and the formal type system that needs a set of transformation tools. Like htmltidy, but without the html.