some code using ur/web, a language/web framework based on dependent types (ie, Coq, Agda, etc) - a login mechanism with salting — http://www.impredicative.com/ur/
cookie c : {Session: string}
table s : {LoggedIn : time, User : string, Session : string}
PRIMARY KEY LoggedIn
table u : {User : string, Salt : string, Password : string}
PRIMARY KEY User
fun main () =
ro <- getCookie c;
xml <- (case ro of
None => return <xml>Not logged in.</xml>
| Some v =>
row <- queryX (SELECT * FROM s WHERE s.Session = {[v.Session]})
(fn r => <xml><tr><td>{[r.S.User]}</td></tr>
</xml>);
return <xml>
Logged in: <table>{row}</table>
<form><submit value="Logout" action={logout}/></form>
</xml>);
return
<xml><body>{xml}
<br/><br/>
<form>
User: <textbox{#User}/><br/>
Password: <password{#Password}/><br/>
<submit action={login}/>
</form><br/><br/>
</body></xml>
and login r =
user <- oneOrNoRows1 (SELECT * FROM u WHERE (u.User = {[r.User]}));
case user of
None => redirect (url (main()))
| Some us =>
if us.Password = Hash.sha512 (Basis.strcat (us.Salt) (r.Password)) then
rs <- Random.str 30;
setCookie c {Value = {Session = rs },
Expires = None,
Secure = False};
dml (INSERT INTO s (LoggedIn, User, Session)
VALUES (CURRENT_TIMESTAMP, {[r.User]}, {[rs]} ));
redirect (url (main()))
else
redirect (url (main()))
and logout () =
ro <- getCookie c;
clearCookie c;
case ro of
None => main()
| Some v =>
dml (DELETE FROM s
WHERE T.Session = {[v.Session]} );
redirect (url (main()))
|